:: Replacing of Variables in Formulas of ZF Theory
:: by Grzegorz Bancerek
::
:: Received August 10, 1990
:: Copyright (c) 1990 Association of Mizar Users
theorem Th1: :: ZF_LANG1:1
theorem Th2: :: ZF_LANG1:2
theorem Th3: :: ZF_LANG1:3
theorem Th4: :: ZF_LANG1:4
theorem :: ZF_LANG1:5
theorem Th6: :: ZF_LANG1:6
theorem :: ZF_LANG1:7
theorem Th8: :: ZF_LANG1:8
theorem Th9: :: ZF_LANG1:9
theorem :: ZF_LANG1:10
theorem :: ZF_LANG1:11
canceled;
theorem :: ZF_LANG1:12
canceled;
theorem :: ZF_LANG1:13
theorem :: ZF_LANG1:14
theorem :: ZF_LANG1:15
for
p being
ZF-formula for
x,
y,
z being
Variable holds
(
All x,
y,
z,
p = All x,
(All y,(All z,p)) &
All x,
y,
z,
p = All x,
y,
(All z,p) ) ;
theorem Th16: :: ZF_LANG1:16
theorem :: ZF_LANG1:17
for
p1,
p2 being
ZF-formula for
x1,
y1,
z1,
x2,
y2,
z2 being
Variable st
All x1,
y1,
z1,
p1 = All x2,
y2,
z2,
p2 holds
(
x1 = x2 &
y1 = y2 &
z1 = z2 &
p1 = p2 )
theorem :: ZF_LANG1:18
canceled;
theorem :: ZF_LANG1:19
for
p,
q being
ZF-formula for
x,
y,
z,
t,
s being
Variable st
All x,
y,
z,
p = All t,
s,
q holds
(
x = t &
y = s &
All z,
p = q )
theorem Th20: :: ZF_LANG1:20
theorem :: ZF_LANG1:21
for
p being
ZF-formula for
x,
y,
z being
Variable holds
(
Ex x,
y,
z,
p = Ex x,
(Ex y,(Ex z,p)) &
Ex x,
y,
z,
p = Ex x,
y,
(Ex z,p) ) ;
theorem :: ZF_LANG1:22
for
p1,
p2 being
ZF-formula for
x1,
y1,
z1,
x2,
y2,
z2 being
Variable st
Ex x1,
y1,
z1,
p1 = Ex x2,
y2,
z2,
p2 holds
(
x1 = x2 &
y1 = y2 &
z1 = z2 &
p1 = p2 )
theorem :: ZF_LANG1:23
canceled;
theorem :: ZF_LANG1:24
for
p,
q being
ZF-formula for
x,
y,
z,
t,
s being
Variable st
Ex x,
y,
z,
p = Ex t,
s,
q holds
(
x = t &
y = s &
Ex z,
p = q )
theorem :: ZF_LANG1:25
for
p being
ZF-formula for
x,
y,
z being
Variable holds
(
All x,
y,
z,
p is
universal &
bound_in (All x,y,z,p) = x &
the_scope_of (All x,y,z,p) = All y,
z,
p )
by Th8, ZF_LANG:16;
theorem :: ZF_LANG1:26
for
p being
ZF-formula for
x,
y,
z being
Variable holds
(
Ex x,
y,
z,
p is
existential &
bound_in (Ex x,y,z,p) = x &
the_scope_of (Ex x,y,z,p) = Ex y,
z,
p )
by Th9, ZF_LANG:22;
theorem :: ZF_LANG1:27
theorem :: ZF_LANG1:28
theorem :: ZF_LANG1:29
theorem :: ZF_LANG1:30
theorem :: ZF_LANG1:31
theorem :: ZF_LANG1:32
theorem :: ZF_LANG1:33
theorem :: ZF_LANG1:34
theorem :: ZF_LANG1:35
theorem :: ZF_LANG1:36
theorem :: ZF_LANG1:37
theorem :: ZF_LANG1:38
theorem :: ZF_LANG1:39
theorem :: ZF_LANG1:40
theorem :: ZF_LANG1:41
theorem :: ZF_LANG1:42
theorem Th43: :: ZF_LANG1:43
theorem Th44: :: ZF_LANG1:44
theorem :: ZF_LANG1:45
canceled;
theorem :: ZF_LANG1:46
theorem :: ZF_LANG1:47
theorem :: ZF_LANG1:48
theorem :: ZF_LANG1:49
theorem :: ZF_LANG1:50
theorem :: ZF_LANG1:51
theorem :: ZF_LANG1:52
theorem :: ZF_LANG1:53
theorem :: ZF_LANG1:54
theorem :: ZF_LANG1:55
theorem :: ZF_LANG1:56
theorem :: ZF_LANG1:57
theorem :: ZF_LANG1:58
theorem :: ZF_LANG1:59
theorem Th60: :: ZF_LANG1:60
theorem :: ZF_LANG1:61
theorem :: ZF_LANG1:62
theorem Th63: :: ZF_LANG1:63
theorem Th64: :: ZF_LANG1:64
theorem Th65: :: ZF_LANG1:65
theorem Th66: :: ZF_LANG1:66
theorem Th67: :: ZF_LANG1:67
theorem :: ZF_LANG1:68
theorem Th69: :: ZF_LANG1:69
theorem :: ZF_LANG1:70
theorem Th71: :: ZF_LANG1:71
theorem Th72: :: ZF_LANG1:72
theorem :: ZF_LANG1:73
theorem Th74: :: ZF_LANG1:74
theorem :: ZF_LANG1:75
:: deftheorem ZF_LANG1:def 1 :
canceled;
:: deftheorem defines ! ZF_LANG1:def 2 :
theorem :: ZF_LANG1:76
canceled;
theorem :: ZF_LANG1:77
canceled;
theorem :: ZF_LANG1:78
canceled;
theorem :: ZF_LANG1:79
canceled;
theorem Th80: :: ZF_LANG1:80
theorem Th81: :: ZF_LANG1:81
theorem Th82: :: ZF_LANG1:82
theorem :: ZF_LANG1:83
theorem :: ZF_LANG1:84
theorem Th85: :: ZF_LANG1:85
theorem :: ZF_LANG1:86
theorem :: ZF_LANG1:87
theorem :: ZF_LANG1:88
canceled;
theorem Th89: :: ZF_LANG1:89
theorem Th90: :: ZF_LANG1:90
theorem Th91: :: ZF_LANG1:91
theorem Th92: :: ZF_LANG1:92
theorem :: ZF_LANG1:93
theorem :: ZF_LANG1:94
theorem :: ZF_LANG1:95
theorem :: ZF_LANG1:96
theorem :: ZF_LANG1:97
theorem :: ZF_LANG1:98
theorem :: ZF_LANG1:99
theorem :: ZF_LANG1:100
theorem :: ZF_LANG1:101
theorem :: ZF_LANG1:102
theorem :: ZF_LANG1:103
theorem :: ZF_LANG1:104
theorem Th105: :: ZF_LANG1:105
theorem Th106: :: ZF_LANG1:106
theorem Th107: :: ZF_LANG1:107
theorem :: ZF_LANG1:108
theorem :: ZF_LANG1:109
theorem :: ZF_LANG1:110
theorem :: ZF_LANG1:111
theorem Th112: :: ZF_LANG1:112
theorem Th113: :: ZF_LANG1:113
theorem :: ZF_LANG1:114
theorem :: ZF_LANG1:115
theorem :: ZF_LANG1:116
theorem :: ZF_LANG1:117
theorem :: ZF_LANG1:118
theorem :: ZF_LANG1:119
theorem :: ZF_LANG1:120
theorem :: ZF_LANG1:121
theorem :: ZF_LANG1:122
theorem Th123: :: ZF_LANG1:123
theorem :: ZF_LANG1:124
theorem :: ZF_LANG1:125
theorem :: ZF_LANG1:126
theorem :: ZF_LANG1:127
theorem :: ZF_LANG1:128
theorem :: ZF_LANG1:129
theorem :: ZF_LANG1:130
theorem :: ZF_LANG1:131
theorem :: ZF_LANG1:132
canceled;
theorem :: ZF_LANG1:133
theorem :: ZF_LANG1:134
theorem :: ZF_LANG1:135
theorem :: ZF_LANG1:136
theorem :: ZF_LANG1:137
theorem :: ZF_LANG1:138
theorem :: ZF_LANG1:139
theorem Th140: :: ZF_LANG1:140
theorem :: ZF_LANG1:141
theorem Th142: :: ZF_LANG1:142
theorem :: ZF_LANG1:143
theorem :: ZF_LANG1:144
theorem :: ZF_LANG1:145
theorem :: ZF_LANG1:146
:: deftheorem defines variables_in ZF_LANG1:def 3 :
theorem :: ZF_LANG1:147
canceled;
theorem Th148: :: ZF_LANG1:148
theorem Th149: :: ZF_LANG1:149
theorem Th150: :: ZF_LANG1:150
theorem Th151: :: ZF_LANG1:151
theorem Th152: :: ZF_LANG1:152
theorem Th153: :: ZF_LANG1:153
theorem Th154: :: ZF_LANG1:154
theorem Th155: :: ZF_LANG1:155
theorem :: ZF_LANG1:156
theorem Th157: :: ZF_LANG1:157
theorem :: ZF_LANG1:158
theorem Th159: :: ZF_LANG1:159
theorem Th160: :: ZF_LANG1:160
theorem Th161: :: ZF_LANG1:161
theorem :: ZF_LANG1:162
theorem :: ZF_LANG1:163
theorem :: ZF_LANG1:164
:: deftheorem Def4 defines / ZF_LANG1:def 4 :
theorem :: ZF_LANG1:165
canceled;
theorem Th166: :: ZF_LANG1:166
for
x1,
x2,
y1,
y2,
z1,
z2 being
Variable holds
(
(x1 '=' x2) / y1,
y2 = z1 '=' z2 iff ( (
x1 <> y1 &
x2 <> y1 &
z1 = x1 &
z2 = x2 ) or (
x1 = y1 &
x2 <> y1 &
z1 = y2 &
z2 = x2 ) or (
x1 <> y1 &
x2 = y1 &
z1 = x1 &
z2 = y2 ) or (
x1 = y1 &
x2 = y1 &
z1 = y2 &
z2 = y2 ) ) )
theorem Th167: :: ZF_LANG1:167
theorem Th168: :: ZF_LANG1:168
for
x1,
x2,
y1,
y2,
z1,
z2 being
Variable holds
(
(x1 'in' x2) / y1,
y2 = z1 'in' z2 iff ( (
x1 <> y1 &
x2 <> y1 &
z1 = x1 &
z2 = x2 ) or (
x1 = y1 &
x2 <> y1 &
z1 = y2 &
z2 = x2 ) or (
x1 <> y1 &
x2 = y1 &
z1 = x1 &
z2 = y2 ) or (
x1 = y1 &
x2 = y1 &
z1 = y2 &
z2 = y2 ) ) )
theorem Th169: :: ZF_LANG1:169
theorem Th170: :: ZF_LANG1:170
Lm1:
for G1, H1, G2, H2 being ZF-formula
for x, y being Variable st G1 = H1 / x,y & G2 = H2 / x,y holds
G1 '&' G2 = (H1 '&' H2) / x,y
Lm2:
for F, H being ZF-formula
for x, y, z, s being Variable st F = H / x,y & ( ( z = s & s <> x ) or ( z = y & s = x ) ) holds
All z,F = (All s,H) / x,y
theorem Th171: :: ZF_LANG1:171
theorem Th172: :: ZF_LANG1:172
theorem Th173: :: ZF_LANG1:173
theorem Th174: :: ZF_LANG1:174
theorem Th175: :: ZF_LANG1:175
theorem Th176: :: ZF_LANG1:176
theorem Th177: :: ZF_LANG1:177
theorem Th178: :: ZF_LANG1:178
theorem Th179: :: ZF_LANG1:179
theorem :: ZF_LANG1:180
theorem :: ZF_LANG1:181
theorem Th182: :: ZF_LANG1:182
theorem Th183: :: ZF_LANG1:183
theorem Th184: :: ZF_LANG1:184
theorem :: ZF_LANG1:185
theorem :: ZF_LANG1:186
theorem :: ZF_LANG1:187
theorem Th188: :: ZF_LANG1:188
theorem Th189: :: ZF_LANG1:189
theorem Th190: :: ZF_LANG1:190
theorem Th191: :: ZF_LANG1:191
theorem :: ZF_LANG1:192
theorem :: ZF_LANG1:193
theorem :: ZF_LANG1:194
theorem :: ZF_LANG1:195
theorem Th196: :: ZF_LANG1:196
theorem :: ZF_LANG1:197
theorem Th198: :: ZF_LANG1:198
theorem :: ZF_LANG1:199
theorem :: ZF_LANG1:200
theorem :: ZF_LANG1:201