Volume 2, 1990

University of Bialystok

Copyright (c) 1990 Association of Mizar Users

### The abstract of the Mizar article:

### Replacing of Variables in Formulas of ZF Theory

**by****Grzegorz Bancerek**- Received August 10, 1990
- MML identifier: ZF_LANG1

- [ Mizar article, MML identifier index ]

environ vocabulary ZF_LANG, FUNCT_1, FINSEQ_1, BOOLE, ZF_MODEL, ARYTM_3, QC_LANG1, RELAT_1, FINSET_1, QC_LANG3; notation TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, SUBSET_1, NUMBERS, XREAL_0, NAT_1, RELAT_1, FUNCT_1, FUNCT_2, FINSEQ_1, FINSET_1, ZF_LANG, ZF_MODEL; constructors ENUMSET1, NAT_1, ZF_MODEL, XREAL_0, MEMBERED, XBOOLE_0; clusters SUBSET_1, FINSET_1, ZF_LANG, RELSET_1, XREAL_0, FINSEQ_1, ARYTM_3, MEMBERED, ZFMISC_1, XBOOLE_0, NUMBERS, ORDINAL2; requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM; begin reserve p,p1,p2,q,r,F,G,G1,G2,H,H1,H2 for ZF-formula, x,x1,x2,y,y1,y2,z,z1,z2,s,t for Variable, a for set, X for set; theorem :: ZF_LANG1:1 Var1 (x '=' y) = x & Var2 (x '=' y) = y; theorem :: ZF_LANG1:2 Var1 (x 'in' y) = x & Var2 (x 'in' y) = y; theorem :: ZF_LANG1:3 the_argument_of 'not' p = p; theorem :: ZF_LANG1:4 the_left_argument_of (p '&' q) = p & the_right_argument_of (p '&' q) = q; theorem :: ZF_LANG1:5 the_left_argument_of (p 'or' q) = p & the_right_argument_of (p 'or' q) = q; theorem :: ZF_LANG1:6 the_antecedent_of (p => q) = p & the_consequent_of (p => q) = q; theorem :: ZF_LANG1:7 the_left_side_of (p <=> q) = p & the_right_side_of (p <=> q) = q; theorem :: ZF_LANG1:8 bound_in All(x,p) = x & the_scope_of All(x,p) = p; theorem :: ZF_LANG1:9 bound_in Ex(x,p) = x & the_scope_of Ex(x,p) = p; theorem :: ZF_LANG1:10 p 'or' q = 'not' p => q; theorem :: ZF_LANG1:11 All(x,y,p) = All(z,q) implies x = z & All(y,p) = q; theorem :: ZF_LANG1:12 Ex(x,y,p) = Ex(z,q) implies x = z & Ex(y,p) = q; theorem :: ZF_LANG1:13 All(x,y,p) is universal & bound_in All(x,y,p) = x & the_scope_of All(x,y,p) = All(y,p); theorem :: ZF_LANG1:14 Ex(x,y,p) is existential & bound_in Ex(x,y,p) = x & the_scope_of Ex(x,y,p) = Ex(y,p); theorem :: ZF_LANG1:15 All(x,y,z,p) = All(x,All(y,All(z,p))) & All(x,y,z,p) = All(x,y,All(z,p)); theorem :: ZF_LANG1:16 All(x1,y1,p1) = All(x2,y2,p2) implies x1 = x2 & y1 = y2 & p1 = p2; theorem :: ZF_LANG1:17 All(x1,y1,z1,p1) = All(x2,y2,z2,p2) implies x1 = x2 & y1 = y2 & z1 = z2 & p1 = p2; theorem :: ZF_LANG1:18 All(x,y,z,p) = All(t,q) implies x = t & All(y,z,p) = q; theorem :: ZF_LANG1:19 All(x,y,z,p) = All(t,s,q) implies x = t & y = s & All(z,p) = q; theorem :: ZF_LANG1:20 Ex(x1,y1,p1) = Ex(x2,y2,p2) implies x1 = x2 & y1 = y2 & p1 = p2; theorem :: ZF_LANG1:21 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 Ex(x1,y1,z1,p1) = Ex(x2,y2,z2,p2) implies x1 = x2 & y1 = y2 & z1 = z2 & p1 = p2; theorem :: ZF_LANG1:23 Ex(x,y,z,p) = Ex(t,q) implies x = t & Ex(y,z,p) = q; theorem :: ZF_LANG1:24 Ex(x,y,z,p) = Ex(t,s,q) implies x = t & y = s & Ex(z,p) = q; theorem :: ZF_LANG1:25 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); theorem :: ZF_LANG1:26 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); theorem :: ZF_LANG1:27 H is disjunctive implies the_left_argument_of H = the_argument_of the_left_argument_of the_argument_of H; theorem :: ZF_LANG1:28 H is disjunctive implies the_right_argument_of H = the_argument_of the_right_argument_of the_argument_of H; theorem :: ZF_LANG1:29 H is conditional implies the_antecedent_of H = the_left_argument_of the_argument_of H; theorem :: ZF_LANG1:30 H is conditional implies the_consequent_of H = the_argument_of the_right_argument_of the_argument_of H; theorem :: ZF_LANG1:31 H is biconditional implies the_left_side_of H = the_antecedent_of the_left_argument_of H & the_left_side_of H = the_consequent_of the_right_argument_of H; theorem :: ZF_LANG1:32 H is biconditional implies the_right_side_of H = the_consequent_of the_left_argument_of H & the_right_side_of H = the_antecedent_of the_right_argument_of H; theorem :: ZF_LANG1:33 H is existential implies bound_in H = bound_in the_argument_of H & the_scope_of H = the_argument_of the_scope_of the_argument_of H; theorem :: ZF_LANG1:34 the_argument_of F 'or' G = 'not' F '&' 'not' G & the_antecedent_of F 'or' G = 'not' F & the_consequent_of F 'or' G = G; theorem :: ZF_LANG1:35 the_argument_of F => G = F '&' 'not' G; theorem :: ZF_LANG1:36 the_left_argument_of F <=> G = F => G & the_right_argument_of F <=> G = G => F; theorem :: ZF_LANG1:37 the_argument_of Ex(x,H) = All(x,'not' H); theorem :: ZF_LANG1:38 H is disjunctive implies H is conditional & H is negative & the_argument_of H is conjunctive & the_left_argument_of the_argument_of H is negative & the_right_argument_of the_argument_of H is negative; theorem :: ZF_LANG1:39 H is conditional implies H is negative & the_argument_of H is conjunctive & the_right_argument_of the_argument_of H is negative; theorem :: ZF_LANG1:40 H is biconditional implies H is conjunctive & the_left_argument_of H is conditional & the_right_argument_of H is conditional; theorem :: ZF_LANG1:41 H is existential implies H is negative & the_argument_of H is universal & the_scope_of the_argument_of H is negative; theorem :: ZF_LANG1:42 not (H is_equality & (H is_membership or H is negative or H is conjunctive or H is universal)) & not (H is_membership & (H is negative or H is conjunctive or H is universal)) & not (H is negative & (H is conjunctive or H is universal)) & not (H is conjunctive & H is universal); theorem :: ZF_LANG1:43 F is_subformula_of G implies len F <= len G; theorem :: ZF_LANG1:44 F is_proper_subformula_of G & G is_subformula_of H or F is_subformula_of G & G is_proper_subformula_of H or F is_subformula_of G & G is_immediate_constituent_of H or F is_immediate_constituent_of G & G is_subformula_of H or F is_proper_subformula_of G & G is_immediate_constituent_of H or F is_immediate_constituent_of G & G is_proper_subformula_of H implies F is_proper_subformula_of H; canceled; theorem :: ZF_LANG1:46 not H is_immediate_constituent_of H; theorem :: ZF_LANG1:47 not (G is_proper_subformula_of H & H is_subformula_of G); theorem :: ZF_LANG1:48 not (G is_proper_subformula_of H & H is_proper_subformula_of G); theorem :: ZF_LANG1:49 not (G is_subformula_of H & H is_immediate_constituent_of G); theorem :: ZF_LANG1:50 not (G is_proper_subformula_of H & H is_immediate_constituent_of G); theorem :: ZF_LANG1:51 'not' F is_subformula_of H implies F is_proper_subformula_of H; theorem :: ZF_LANG1:52 F '&' G is_subformula_of H implies F is_proper_subformula_of H & G is_proper_subformula_of H; theorem :: ZF_LANG1:53 All(x,H) is_subformula_of F implies H is_proper_subformula_of F; theorem :: ZF_LANG1:54 F '&' 'not' G is_proper_subformula_of F => G & F is_proper_subformula_of F => G & 'not' G is_proper_subformula_of F => G & G is_proper_subformula_of F => G; theorem :: ZF_LANG1:55 'not' F '&' 'not' G is_proper_subformula_of F 'or' G & 'not' F is_proper_subformula_of F 'or' G & 'not' G is_proper_subformula_of F 'or' G & F is_proper_subformula_of F 'or' G & G is_proper_subformula_of F 'or' G; theorem :: ZF_LANG1:56 All(x,'not' H) is_proper_subformula_of Ex(x,H) & 'not' H is_proper_subformula_of Ex(x,H); theorem :: ZF_LANG1:57 G is_subformula_of H iff G in Subformulae H; theorem :: ZF_LANG1:58 G in Subformulae H implies Subformulae G c= Subformulae H; theorem :: ZF_LANG1:59 H in Subformulae H; theorem :: ZF_LANG1:60 Subformulae (F => G) = Subformulae F \/ Subformulae G \/ { 'not' G, F '&' 'not' G, F => G }; theorem :: ZF_LANG1:61 Subformulae (F 'or' G) = Subformulae F \/ Subformulae G \/ {'not' G, 'not' F, 'not' F '&' 'not' G, F 'or' G}; theorem :: ZF_LANG1:62 Subformulae (F <=> G) = Subformulae F \/ Subformulae G \/ { 'not' G, F '&' 'not' G, F => G, 'not' F, G '&' 'not' F, G => F, F <=> G }; theorem :: ZF_LANG1:63 Free (x '=' y) = {x,y}; theorem :: ZF_LANG1:64 Free (x 'in' y) = {x,y}; theorem :: ZF_LANG1:65 Free ('not' p) = Free p; theorem :: ZF_LANG1:66 Free (p '&' q) = Free p \/ Free q; theorem :: ZF_LANG1:67 Free All(x,p) = Free p \ {x}; theorem :: ZF_LANG1:68 Free (p 'or' q) = Free p \/ Free q; theorem :: ZF_LANG1:69 Free (p => q) = Free p \/ Free q; theorem :: ZF_LANG1:70 Free (p <=> q) = Free p \/ Free q; theorem :: ZF_LANG1:71 Free Ex(x,p) = Free p \ {x}; theorem :: ZF_LANG1:72 Free All(x,y,p) = Free p \ {x,y}; theorem :: ZF_LANG1:73 Free All(x,y,z,p) = Free p \ {x,y,z}; theorem :: ZF_LANG1:74 Free Ex(x,y,p) = Free p \ {x,y}; theorem :: ZF_LANG1:75 Free Ex(x,y,z,p) = Free p \ {x,y,z}; scheme ZF_Induction { P[ZF-formula] } : for H holds P[H] provided for x1,x2 holds P[x1 '=' x2] & P[x1 'in' x2] and for H st P[H] holds P['not' H] and for H1,H2 st P[H1] & P[H2] holds P[H1 '&' H2] and for H,x st P[H] holds P[All(x,H)]; reserve M,E for non empty set, e for Element of E, m,m' for Element of M, f,g for Function of VAR,E, v,v' for Function of VAR,M; definition let E,f,x,e; func f / (x,e) -> Function of VAR,E means :: ZF_LANG1:def 1 it.x = e & for y st it.y <> f.y holds x = y; end; definition let D,D1,D2 be non empty set, f be Function of D,D1; assume D1 c= D2; func D2!f -> Function of D,D2 equals :: ZF_LANG1:def 2 f; end; canceled 2; theorem :: ZF_LANG1:78 (v/(x,m'))/(x,m) = v/(x,m) & v/(x,v.x) = v; theorem :: ZF_LANG1:79 x <> y implies (v/(x,m))/(y,m') = (v/(y,m'))/(x,m); theorem :: ZF_LANG1:80 M,v |= All(x,H) iff for m holds M,v/(x,m) |= H; theorem :: ZF_LANG1:81 M,v |= All(x,H) iff M,v/(x,m) |= All(x,H); theorem :: ZF_LANG1:82 M,v |= Ex(x,H) iff ex m st M,v/(x,m) |= H; theorem :: ZF_LANG1:83 M,v |= Ex(x,H) iff M,v/(x,m) |= Ex(x,H); theorem :: ZF_LANG1:84 for v,v' st for x st x in Free H holds v'.x = v.x holds M,v |= H implies M,v' |= H; theorem :: ZF_LANG1:85 Free H is finite; definition let H; cluster Free H -> finite; end; reserve i,j for Nat; theorem :: ZF_LANG1:86 x.i = x.j implies i = j; theorem :: ZF_LANG1:87 ex i st x = x.i; canceled; theorem :: ZF_LANG1:89 M,v |= x '=' x; theorem :: ZF_LANG1:90 M |= x '=' x; theorem :: ZF_LANG1:91 not M,v |= x 'in' x; theorem :: ZF_LANG1:92 not M |= x 'in' x & M |= 'not' x 'in' x; theorem :: ZF_LANG1:93 M |= x '=' y iff x = y or ex a st {a} = M; theorem :: ZF_LANG1:94 M |= 'not' x 'in' y iff x = y or for X st X in M holds X misses M; theorem :: ZF_LANG1:95 H is_equality implies (M,v |= H iff v.Var1 H = v.Var2 H); theorem :: ZF_LANG1:96 H is_membership implies (M,v |= H iff v.Var1 H in v.Var2 H); theorem :: ZF_LANG1:97 H is negative implies (M,v |= H iff not M,v |= the_argument_of H); theorem :: ZF_LANG1:98 H is conjunctive implies (M,v |= H iff M,v |= the_left_argument_of H & M,v |= the_right_argument_of H); theorem :: ZF_LANG1:99 H is universal implies (M,v |= H iff for m holds M,v/(bound_in H,m) |= the_scope_of H); theorem :: ZF_LANG1:100 H is disjunctive implies (M,v |= H iff M,v |= the_left_argument_of H or M,v |= the_right_argument_of H); theorem :: ZF_LANG1:101 H is conditional implies (M,v |= H iff (M,v |= the_antecedent_of H implies M,v |= the_consequent_of H)); theorem :: ZF_LANG1:102 H is biconditional implies (M,v |= H iff (M,v |= the_left_side_of H iff M,v |= the_right_side_of H)); theorem :: ZF_LANG1:103 H is existential implies (M,v |= H iff ex m st M,v/(bound_in H,m) |= the_scope_of H); theorem :: ZF_LANG1:104 M |= Ex(x,H) iff for v ex m st M,v/(x,m) |= H; theorem :: ZF_LANG1:105 M |= H implies M |= Ex(x,H); theorem :: ZF_LANG1:106 M |= H iff M |= All(x,y,H); theorem :: ZF_LANG1:107 M |= H implies M |= Ex(x,y,H); theorem :: ZF_LANG1:108 M |= H iff M |= All(x,y,z,H); theorem :: ZF_LANG1:109 M |= H implies M |= Ex(x,y,z,H); :: :: Axioms of Logic :: theorem :: ZF_LANG1:110 M,v |= (p <=> q) => (p => q) & M |= (p <=> q) => (p => q); theorem :: ZF_LANG1:111 M,v |= (p <=> q) => (q => p) & M |= (p <=> q) => (q => p); theorem :: ZF_LANG1:112 M |= (p => q) => ((q => r) => (p => r)); theorem :: ZF_LANG1:113 M,v |= p => q & M,v |= q => r implies M,v |= p => r; theorem :: ZF_LANG1:114 M |= p => q & M |= q => r implies M |= p => r; theorem :: ZF_LANG1:115 M,v |= (p => q) '&' (q => r) => (p => r) & M |= (p => q) '&' (q => r) => (p => r); theorem :: ZF_LANG1:116 M,v |= p => (q => p) & M |= p => (q => p); theorem :: ZF_LANG1:117 M,v |= (p => (q => r)) => ((p => q) => (p => r)) & M |= (p => (q => r)) => ((p => q) => (p => r)); theorem :: ZF_LANG1:118 M,v |= p '&' q => p & M |= p '&' q => p; theorem :: ZF_LANG1:119 M,v |= p '&' q => q & M |= p '&' q => q; theorem :: ZF_LANG1:120 M,v |= p '&' q => q '&' p & M |= p '&' q => q '&' p; theorem :: ZF_LANG1:121 M,v |= p => p '&' p & M |= p => p '&' p; theorem :: ZF_LANG1:122 M,v |= (p => q) => ((p => r) => (p => q '&' r)) & M |= (p => q) => ((p => r) => (p => q '&' r)); theorem :: ZF_LANG1:123 M,v |= p => p 'or' q & M |= p => p 'or' q; theorem :: ZF_LANG1:124 M,v |= q => p 'or' q & M |= q => p 'or' q; theorem :: ZF_LANG1:125 M,v |= p 'or' q => q 'or' p & M |= p 'or' q => q 'or' p; theorem :: ZF_LANG1:126 M,v |= p => p 'or' p & M |= p => p 'or' p; theorem :: ZF_LANG1:127 M,v |= (p => r) => ((q => r) => (p 'or' q => r)) & M |= (p => r) => ((q => r) => (p 'or' q => r)); theorem :: ZF_LANG1:128 M,v |= (p => r) '&' (q => r) => (p 'or' q => r) & M |= (p => r) '&' (q => r) => (p 'or' q => r); theorem :: ZF_LANG1:129 M,v |= (p => 'not' q) => (q => 'not' p) & M |= (p => 'not' q) => (q => 'not' p); theorem :: ZF_LANG1:130 M,v |= 'not' p => (p => q) & M |= 'not' p => (p => q); theorem :: ZF_LANG1:131 M,v |= (p => q) '&' (p => 'not' q) => 'not' p & M |= (p => q) '&' (p => 'not' q) => 'not' p; canceled; theorem :: ZF_LANG1:133 M |= p => q & M |= p implies M |= q; theorem :: ZF_LANG1:134 M,v |= 'not'(p '&' q) => 'not' p 'or' 'not' q & M |= 'not'(p '&' q) => 'not' p 'or' 'not' q; theorem :: ZF_LANG1:135 M,v |= 'not' p 'or' 'not' q => 'not'(p '&' q) & M |= 'not' p 'or' 'not' q => 'not'(p '&' q); theorem :: ZF_LANG1:136 M,v |= 'not'(p 'or' q) => 'not' p '&' 'not' q & M |= 'not'(p 'or' q) => 'not' p '&' 'not' q; theorem :: ZF_LANG1:137 M,v |= 'not' p '&' 'not' q => 'not'(p 'or' q) & M |= 'not' p '&' 'not' q => 'not'(p 'or' q); theorem :: ZF_LANG1:138 M |= All(x,H) => H; theorem :: ZF_LANG1:139 M |= H => Ex(x,H); theorem :: ZF_LANG1:140 not x in Free H1 implies M |= All(x,H1 => H2) => (H1 => All(x,H2)); theorem :: ZF_LANG1:141 not x in Free H1 & M |= H1 => H2 implies M |= H1 => All(x,H2); theorem :: ZF_LANG1:142 not x in Free H2 implies M |= All(x,H1 => H2) => (Ex(x,H1) => H2); theorem :: ZF_LANG1:143 not x in Free H2 & M |= H1 => H2 implies M |= Ex(x,H1) => H2; theorem :: ZF_LANG1:144 M |= H1 => All(x,H2) implies M |= H1 => H2; theorem :: ZF_LANG1:145 M |= Ex(x,H1) => H2 implies M |= H1 => H2; theorem :: ZF_LANG1:146 WFF c= bool [:NAT,NAT:]; :: :: Variables in ZF-formula :: definition let H; func variables_in H -> set equals :: ZF_LANG1:def 3 rng H \ { 0,1,2,3,4 }; end; canceled; theorem :: ZF_LANG1:148 x <> 0 & x <> 1 & x <> 2 & x <> 3 & x <> 4; theorem :: ZF_LANG1:149 not x in { 0,1,2,3,4 }; theorem :: ZF_LANG1:150 a in variables_in H implies a <> 0 & a <> 1 & a <> 2 & a <> 3 & a <> 4; theorem :: ZF_LANG1:151 variables_in x '=' y = {x,y}; theorem :: ZF_LANG1:152 variables_in x 'in' y = {x,y}; theorem :: ZF_LANG1:153 variables_in 'not' H = variables_in H; theorem :: ZF_LANG1:154 variables_in H1 '&' H2 = variables_in H1 \/ variables_in H2; theorem :: ZF_LANG1:155 variables_in All(x,H) = variables_in H \/ {x}; theorem :: ZF_LANG1:156 variables_in H1 'or' H2 = variables_in H1 \/ variables_in H2; theorem :: ZF_LANG1:157 variables_in H1 => H2 = variables_in H1 \/ variables_in H2; theorem :: ZF_LANG1:158 variables_in H1 <=> H2 = variables_in H1 \/ variables_in H2; theorem :: ZF_LANG1:159 variables_in Ex(x,H) = variables_in H \/ {x}; theorem :: ZF_LANG1:160 variables_in All(x,y,H) = variables_in H \/ {x,y}; theorem :: ZF_LANG1:161 variables_in Ex(x,y,H) = variables_in H \/ {x,y}; theorem :: ZF_LANG1:162 variables_in All(x,y,z,H) = variables_in H \/ {x,y,z}; theorem :: ZF_LANG1:163 variables_in Ex(x,y,z,H) = variables_in H \/ {x,y,z}; theorem :: ZF_LANG1:164 Free H c= variables_in H; definition let H; redefine func variables_in H -> non empty Subset of VAR; end; definition let H,x,y; func H/(x,y) -> Function means :: ZF_LANG1:def 4 dom it = dom H & for a st a in dom H holds (H.a = x implies it.a = y) & (H.a <> x implies it.a = H.a); end; canceled; theorem :: ZF_LANG1:166 (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 :: ZF_LANG1:167 ex z1,z2 st (x1 '=' x2)/(y1,y2) = z1 '=' z2; theorem :: ZF_LANG1:168 (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 :: ZF_LANG1:169 ex z1,z2 st (x1 'in' x2)/(y1,y2) = z1 'in' z2; theorem :: ZF_LANG1:170 'not' F = ('not' H)/(x,y) iff F = H/(x,y); theorem :: ZF_LANG1:171 H/(x,y) in WFF; definition let H,x,y; redefine func H/(x,y) -> ZF-formula; end; theorem :: ZF_LANG1:172 G1 '&' G2 = (H1 '&' H2)/(x,y) iff G1 = H1/(x,y) & G2 = H2/(x,y); theorem :: ZF_LANG1:173 z <> x implies (All(z,G) = All(z,H)/(x,y) iff G = H/(x,y)); theorem :: ZF_LANG1:174 All(y,G) = All(x,H)/(x,y) iff G = H/(x,y); theorem :: ZF_LANG1:175 G1 'or' G2 = (H1 'or' H2)/(x,y) iff G1 = H1/(x,y) & G2 = H2/(x,y); theorem :: ZF_LANG1:176 G1 => G2 = (H1 => H2)/(x,y) iff G1 = H1/(x,y) & G2 = H2/(x,y); theorem :: ZF_LANG1:177 G1 <=> G2 = (H1 <=> H2)/(x,y) iff G1 = H1/(x,y) & G2 = H2/(x,y); theorem :: ZF_LANG1:178 z <> x implies (Ex(z,G) = Ex(z,H)/(x,y) iff G = H/(x,y)); theorem :: ZF_LANG1:179 Ex(y,G) = Ex(x,H)/(x,y) iff G = H/(x,y); theorem :: ZF_LANG1:180 H is_equality iff H/(x,y) is_equality; theorem :: ZF_LANG1:181 H is_membership iff H/(x,y) is_membership; theorem :: ZF_LANG1:182 H is negative iff H/(x,y) is negative; theorem :: ZF_LANG1:183 H is conjunctive iff H/(x,y) is conjunctive; theorem :: ZF_LANG1:184 H is universal iff H/(x,y) is universal; theorem :: ZF_LANG1:185 H is negative implies the_argument_of (H/(x,y)) = (the_argument_of H)/(x,y); theorem :: ZF_LANG1:186 H is conjunctive implies the_left_argument_of (H/(x,y)) = (the_left_argument_of H)/(x,y) & the_right_argument_of (H/(x,y)) = (the_right_argument_of H)/(x,y); theorem :: ZF_LANG1:187 H is universal implies the_scope_of (H/(x,y)) = (the_scope_of H)/(x,y) & (bound_in H = x implies bound_in (H/(x,y)) = y) & (bound_in H <> x implies bound_in (H/(x,y)) = bound_in H); theorem :: ZF_LANG1:188 H is disjunctive iff H/(x,y) is disjunctive; theorem :: ZF_LANG1:189 H is conditional iff H/(x,y) is conditional; theorem :: ZF_LANG1:190 H is biconditional implies H/(x,y) is biconditional; theorem :: ZF_LANG1:191 H is existential iff H/(x,y) is existential; theorem :: ZF_LANG1:192 H is disjunctive implies the_left_argument_of (H/(x,y)) = (the_left_argument_of H)/(x,y) & the_right_argument_of (H/(x,y)) = (the_right_argument_of H)/(x,y); theorem :: ZF_LANG1:193 H is conditional implies the_antecedent_of (H/(x,y)) = (the_antecedent_of H)/(x,y) & the_consequent_of (H/(x,y)) = (the_consequent_of H)/(x,y); theorem :: ZF_LANG1:194 H is biconditional implies the_left_side_of (H/(x,y)) = (the_left_side_of H)/(x,y) & the_right_side_of (H/(x,y)) = (the_right_side_of H)/(x,y); theorem :: ZF_LANG1:195 H is existential implies the_scope_of (H/(x,y)) = (the_scope_of H)/(x,y) & (bound_in H = x implies bound_in (H/(x,y)) = y) & (bound_in H <> x implies bound_in (H/(x,y)) = bound_in H); theorem :: ZF_LANG1:196 not x in variables_in H implies H/(x,y) = H; theorem :: ZF_LANG1:197 H/(x,x) = H; theorem :: ZF_LANG1:198 x <> y implies not x in variables_in (H/(x,y)); theorem :: ZF_LANG1:199 x in variables_in H implies y in variables_in (H/(x,y)); theorem :: ZF_LANG1:200 x <> y implies (H/(x,y))/(x,z) = H/(x,y); theorem :: ZF_LANG1:201 variables_in (H/(x,y)) c= (variables_in H \ {x}) \/ {y};

Back to top