:: Replacing of Variables in Formulas of ZF Theory
::  by Grzegorz Bancerek
::
:: Received August 10, 1990
:: Copyright (c) 1990-2021 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies NUMBERS, ZF_LANG, XBOOLEAN, XXREAL_0, BVFUNC_2, CLASSES2,
      FUNCT_1, CARD_1, FINSEQ_1, ARYTM_3, TARSKI, XBOOLE_0, ZF_MODEL, SUBSET_1,
      REALSET1, RELAT_1, FUNCT_4, FINSET_1, NAT_1, ZFMISC_1, ORDINAL4,
      ZF_LANG1;
 notations TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS,
      XCMPLX_0, NAT_1, RELAT_1, FUNCT_1, FUNCT_2, FINSEQ_1, FINSET_1, ZF_LANG,
      ZF_MODEL, XXREAL_0, FUNCT_7, TREES_3;
 constructors ENUMSET1, XXREAL_0, XREAL_0, NAT_1, ZF_MODEL, FUNCT_7, RELSET_1,
      NUMBERS, TREES_3;
 registrations XBOOLE_0, SUBSET_1, ORDINAL1, RELSET_1, FINSET_1, XXREAL_0,
      NAT_1, FINSEQ_1, ZF_LANG, XCMPLX_0;
 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,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) is universal & bound_in All(x,y,p) = x & the_scope_of All(x
  ,y,p) = All(y,p);

theorem :: ZF_LANG1:12
  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:13
  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:14
  All(x1,y1,p1) = All(x2,y2,p2) implies x1 = x2 & y1 = y2 & p1 = p2;

theorem :: ZF_LANG1:15
  All(x1,y1,z1,p1) = All(x2,y2,z2,p2) implies x1 = x2 & y1 = y2 & z1 =
  z2 & p1 = p2;

theorem :: ZF_LANG1:16
  All(x,y,z,p) = All(t,s,q) implies x = t & y = s & All(z,p) = q;

theorem :: ZF_LANG1:17
  Ex(x1,y1,p1) = Ex(x2,y2,p2) implies x1 = x2 & y1 = y2 & p1 = p2;

theorem :: ZF_LANG1:18
  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:19
  Ex(x1,y1,z1,p1) = Ex(x2,y2,z2,p2) implies x1 = x2 & y1 = y2 & z1 = z2
  & p1 = p2;

theorem :: ZF_LANG1:20
  Ex(x,y,z,p) = Ex(t,s,q) implies x = t & y = s & Ex(z,p) = q;

theorem :: ZF_LANG1:21
  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:22
  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:23
  H is disjunctive implies the_left_argument_of H = the_argument_of
  the_left_argument_of the_argument_of H;

theorem :: ZF_LANG1:24
  H is disjunctive implies the_right_argument_of H = the_argument_of
  the_right_argument_of the_argument_of H;

theorem :: ZF_LANG1:25
  H is conditional implies the_antecedent_of H = the_left_argument_of
  the_argument_of H;

theorem :: ZF_LANG1:26
  H is conditional implies the_consequent_of H = the_argument_of
  the_right_argument_of the_argument_of H;

theorem :: ZF_LANG1:27
  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:28
  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:29
  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:30
  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:31
  the_argument_of F => G = F '&' 'not' G;

theorem :: ZF_LANG1:32
  the_left_argument_of F <=> G = F => G & the_right_argument_of F <=> G
  = G => F;

theorem :: ZF_LANG1:33
  the_argument_of Ex(x,H) = All(x,'not' H);

theorem :: ZF_LANG1:34
  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:35
  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:36
  H is biconditional implies H is conjunctive & the_left_argument_of H
  is conditional & the_right_argument_of H is conditional;

theorem :: ZF_LANG1:37
  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:38
  not (H is being_equality & (H is being_membership or H is negative or
  H is conjunctive or H is universal)) & not (H is being_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:39
  F is_subformula_of G implies len F <= len G;

theorem :: ZF_LANG1:40
  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;

theorem :: ZF_LANG1:41
  not H is_immediate_constituent_of H;

theorem :: ZF_LANG1:42
  not (G is_proper_subformula_of H & H is_subformula_of G);

theorem :: ZF_LANG1:43
  not (G is_proper_subformula_of H & H is_proper_subformula_of G);

theorem :: ZF_LANG1:44
  not (G is_subformula_of H & H is_immediate_constituent_of G);

theorem :: ZF_LANG1:45
  not (G is_proper_subformula_of H & H is_immediate_constituent_of G);

theorem :: ZF_LANG1:46
  'not' F is_subformula_of H implies F is_proper_subformula_of H;

theorem :: ZF_LANG1:47
  F '&' G is_subformula_of H implies F is_proper_subformula_of H & G
  is_proper_subformula_of H;

theorem :: ZF_LANG1:48
  All(x,H) is_subformula_of F implies H is_proper_subformula_of F;

theorem :: ZF_LANG1:49
  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:50
  '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:51
  All(x,'not' H) is_proper_subformula_of Ex(x,H) & 'not' H
  is_proper_subformula_of Ex(x,H);

theorem :: ZF_LANG1:52
  G is_subformula_of H iff G in Subformulae H;

theorem :: ZF_LANG1:53
  G in Subformulae H implies Subformulae G c= Subformulae H;

theorem :: ZF_LANG1:54
  H in Subformulae H;

theorem :: ZF_LANG1:55
  Subformulae (F => G) = Subformulae F \/ Subformulae G \/ { 'not'
  G, F '&' 'not' G, F => G };

theorem :: ZF_LANG1:56
  Subformulae (F 'or' G) = Subformulae F \/ Subformulae G \/ {'not' G,
  'not' F, 'not' F '&' 'not' G, F 'or' G};

theorem :: ZF_LANG1:57
  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:58
  Free (x '=' y) = {x,y};

theorem :: ZF_LANG1:59
  Free (x 'in' y) = {x,y};

theorem :: ZF_LANG1:60
  Free ('not' p) = Free p;

theorem :: ZF_LANG1:61
  Free (p '&' q) = Free p \/ Free q;

theorem :: ZF_LANG1:62
  Free All(x,p) = Free p \ {x};

theorem :: ZF_LANG1:63
  Free (p 'or' q) = Free p \/ Free q;

theorem :: ZF_LANG1:64
  Free (p => q) = Free p \/ Free q;

theorem :: ZF_LANG1:65
  Free (p <=> q) = Free p \/ Free q;

theorem :: ZF_LANG1:66
  Free Ex(x,p) = Free p \ {x};

theorem :: ZF_LANG1:67
  Free All(x,y,p) = Free p \ {x,y};

theorem :: ZF_LANG1:68
  Free All(x,y,z,p) = Free p \ {x,y,z};

theorem :: ZF_LANG1:69
  Free Ex(x,y,p) = Free p \ {x,y};

theorem :: ZF_LANG1:70
  Free Ex(x,y,z,p) = Free p \ {x,y,z};

scheme :: ZF_LANG1:sch 1
  ZFInduction { 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 for non empty set,
  m,m9 for Element of M,
  v,v9 for Function of VAR,M;

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 1
  f;
end;

notation
  let E be non empty set, f be Function of VAR,E, x be Variable, e be Element
  of E;
  synonym f / (x,e) for f+*(x,e);
end;

definition
  let E be non empty set, f be Function of VAR,E, x be Variable, e be Element
  of E;
  redefine func f/(x,e) -> Function of VAR, E;
end;

theorem :: ZF_LANG1:71
  M,v |= All(x,H) iff for m holds M,v/(x,m) |= H;

theorem :: ZF_LANG1:72
  M,v |= All(x,H) iff M,v/(x,m) |= All(x,H);

theorem :: ZF_LANG1:73
  M,v |= Ex(x,H) iff ex m st M,v/(x,m) |= H;

theorem :: ZF_LANG1:74
  M,v |= Ex(x,H) iff M,v/(x,m) |= Ex(x,H);

theorem :: ZF_LANG1:75
  for v,v9 st for x st x in Free H holds v9.x = v.x holds M,v |= H
  implies M,v9 |= H;

registration
  let H;
  cluster Free H -> finite;
end;

reserve i,j for Element of NAT;

theorem :: ZF_LANG1:76
  x.i = x.j implies i = j;

theorem :: ZF_LANG1:77
  ex i st x = x.i;

theorem :: ZF_LANG1:78
  M,v |= x '=' x;

theorem :: ZF_LANG1:79
  M |= x '=' x;

theorem :: ZF_LANG1:80
  not M,v |= x 'in' x;

theorem :: ZF_LANG1:81
  not M |= x 'in' x & M |= 'not' x 'in' x;

theorem :: ZF_LANG1:82
  M |= x '=' y iff x = y or ex a st {a} = M;

theorem :: ZF_LANG1:83
  M |= 'not' x 'in' y iff x = y or for X st X in M holds X misses M;

theorem :: ZF_LANG1:84
  H is being_equality implies (M,v |= H iff v.Var1 H = v.Var2 H);

theorem :: ZF_LANG1:85
  H is being_membership implies (M,v |= H iff v.Var1 H in v.Var2 H);

theorem :: ZF_LANG1:86
  H is negative implies (M,v |= H iff not M,v |= the_argument_of H);

theorem :: ZF_LANG1:87
  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:88
  H is universal implies (M,v |= H iff for m holds M,v/(bound_in H,m) |=
  the_scope_of H);

theorem :: ZF_LANG1:89
  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:90
  H is conditional implies (M,v |= H iff (M,v |= the_antecedent_of H
  implies M,v |= the_consequent_of H));

theorem :: ZF_LANG1:91
  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:92
  H is existential implies (M,v |= H iff ex m st M,v/(bound_in H,m) |=
  the_scope_of H);

theorem :: ZF_LANG1:93
  M |= Ex(x,H) iff for v ex m st M,v/(x,m) |= H;

theorem :: ZF_LANG1:94
  M |= H implies M |= Ex(x,H);

theorem :: ZF_LANG1:95
  M |= H iff M |= All(x,y,H);

theorem :: ZF_LANG1:96
  M |= H implies M |= Ex(x,y,H);

theorem :: ZF_LANG1:97
  M |= H iff M |= All(x,y,z,H);

theorem :: ZF_LANG1:98
  M |= H implies M |= Ex(x,y,z,H);

::
:: Axioms of Logic
::

theorem :: ZF_LANG1:99
  M,v |= (p <=> q) => (p => q) & M |= (p <=> q) => (p => q);

theorem :: ZF_LANG1:100
  M,v |= (p <=> q) => (q => p) & M |= (p <=> q) => (q => p);

theorem :: ZF_LANG1:101
  M |= (p => q) => ((q => r) => (p => r));

theorem :: ZF_LANG1:102
  M,v |= p => q & M,v |= q => r implies M,v |= p => r;

theorem :: ZF_LANG1:103
  M |= p => q & M |= q => r implies M |= p => r;

theorem :: ZF_LANG1:104
  M,v |= (p => q) '&' (q => r) => (p => r) & M |= (p => q) '&' (q => r)
  => (p => r);

theorem :: ZF_LANG1:105
  M,v |= p => (q => p) & M |= p => (q => p);

theorem :: ZF_LANG1:106
  M,v |= (p => (q => r)) => ((p => q) => (p => r)) & M |= (p => (q => r)
  ) => ((p => q) => (p => r));

theorem :: ZF_LANG1:107
  M,v |= p '&' q => p & M |= p '&' q => p;

theorem :: ZF_LANG1:108
  M,v |= p '&' q => q & M |= p '&' q => q;

theorem :: ZF_LANG1:109
  M,v |= p '&' q => q '&' p & M |= p '&' q => q '&' p;

theorem :: ZF_LANG1:110
  M,v |= p => p '&' p & M |= p => p '&' p;

theorem :: ZF_LANG1:111
  M,v |= (p => q) => ((p => r) => (p => q '&' r)) & M |= (p => q) => ((p
  => r) => (p => q '&' r));

theorem :: ZF_LANG1:112
  M,v |= p => p 'or' q & M |= p => p 'or' q;

theorem :: ZF_LANG1:113
  M,v |= q => p 'or' q & M |= q => p 'or' q;

theorem :: ZF_LANG1:114
  M,v |= p 'or' q => q 'or' p & M |= p 'or' q => q 'or' p;

theorem :: ZF_LANG1:115
  M,v |= p => p 'or' p & M |= p => p 'or' p;

theorem :: ZF_LANG1:116
  M,v |= (p => r) => ((q => r) => (p 'or' q => r)) & M |= (p => r) => ((
  q => r) => (p 'or' q => r));

theorem :: ZF_LANG1:117
  M,v |= (p => r) '&' (q => r) => (p 'or' q => r) & M |= (p => r) '&' (q
  => r) => (p 'or' q => r);

theorem :: ZF_LANG1:118
  M,v |= (p => 'not' q) => (q => 'not' p) & M |= (p => 'not' q) => (q =>
  'not' p);

theorem :: ZF_LANG1:119
  M,v |= 'not' p => (p => q) & M |= 'not' p => (p => q);

theorem :: ZF_LANG1:120
  M,v |= (p => q) '&' (p => 'not' q) => 'not' p & M |= (p => q) '&' (p
  => 'not' q) => 'not' p;

theorem :: ZF_LANG1:121
  M |= p => q & M |= p implies M |= q;

theorem :: ZF_LANG1:122
  M,v |= 'not'(p '&' q) => 'not' p 'or' 'not' q & M |= 'not'(p '&' q) =>
  'not' p 'or' 'not' q;

theorem :: ZF_LANG1:123
  M,v |= 'not' p 'or' 'not' q => 'not'(p '&' q) & M |= 'not' p 'or'
  'not' q => 'not'(p '&' q);

theorem :: ZF_LANG1:124
  M,v |= 'not'(p 'or' q) => 'not' p '&' 'not' q & M |= 'not'(p 'or' q)
  => 'not' p '&' 'not' q;

theorem :: ZF_LANG1:125
  M,v |= 'not' p '&' 'not' q => 'not'(p 'or' q) & M |= 'not' p '&' 'not'
  q => 'not'(p 'or' q);

theorem :: ZF_LANG1:126
  M |= All(x,H) => H;

theorem :: ZF_LANG1:127
  M |= H => Ex(x,H);

theorem :: ZF_LANG1:128
  not x in Free H1 implies M |= All(x,H1 => H2) => (H1 => All(x, H2));

theorem :: ZF_LANG1:129
  not x in Free H1 & M |= H1 => H2 implies M |= H1 => All(x,H2);

theorem :: ZF_LANG1:130
  not x in Free H2 implies M |= All(x,H1 => H2) => (Ex(x,H1) => H2);

theorem :: ZF_LANG1:131
  not x in Free H2 & M |= H1 => H2 implies M |= Ex(x,H1) => H2;

theorem :: ZF_LANG1:132
  M |= H1 => All(x,H2) implies M |= H1 => H2;

theorem :: ZF_LANG1:133
  M |= Ex(x,H1) => H2 implies M |= H1 => H2;

theorem :: ZF_LANG1:134
  WFF c= bool [:NAT,NAT:];

::
:: Variables in ZF-formula
::

definition
  let H;
  func variables_in H -> set equals
:: ZF_LANG1:def 2
  rng H \ { 0,1,2,3,4 };
end;

theorem :: ZF_LANG1:135
  x <> 0 & x <> 1 & x <> 2 & x <> 3 & x <> 4;

theorem :: ZF_LANG1:136
  not x in { 0,1,2,3,4 };

theorem :: ZF_LANG1:137
  a in variables_in H implies a <> 0 & a <> 1 & a <> 2 & a <> 3 & a <> 4;

theorem :: ZF_LANG1:138
  variables_in x '=' y = {x,y};

theorem :: ZF_LANG1:139
  variables_in x 'in' y = {x,y};

theorem :: ZF_LANG1:140
  variables_in 'not' H = variables_in H;

theorem :: ZF_LANG1:141
  variables_in H1 '&' H2 = variables_in H1 \/ variables_in H2;

theorem :: ZF_LANG1:142
  variables_in All(x,H) = variables_in H \/ {x};

theorem :: ZF_LANG1:143
  variables_in H1 'or' H2 = variables_in H1 \/ variables_in H2;

theorem :: ZF_LANG1:144
  variables_in H1 => H2 = variables_in H1 \/ variables_in H2;

theorem :: ZF_LANG1:145
  variables_in H1 <=> H2 = variables_in H1 \/ variables_in H2;

theorem :: ZF_LANG1:146
  variables_in Ex(x,H) = variables_in H \/ {x};

theorem :: ZF_LANG1:147
  variables_in All(x,y,H) = variables_in H \/ {x,y};

theorem :: ZF_LANG1:148
  variables_in Ex(x,y,H) = variables_in H \/ {x,y};

theorem :: ZF_LANG1:149
  variables_in All(x,y,z,H) = variables_in H \/ {x,y,z};

theorem :: ZF_LANG1:150
  variables_in Ex(x,y,z,H) = variables_in H \/ {x,y,z};

theorem :: ZF_LANG1:151
  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 3

  dom it = dom H & for a being object st a in dom H
  holds (H.a = x implies it.a = y) & (H.a <> x implies it.a = H.a);
end;

theorem :: ZF_LANG1:152
  (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:153
  ex z1,z2 st (x1 '=' x2)/(y1,y2) = z1 '=' z2;

theorem :: ZF_LANG1:154
  (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:155
  ex z1,z2 st (x1 'in' x2)/(y1,y2) = z1 'in' z2;

theorem :: ZF_LANG1:156
  'not' F = ('not' H)/(x,y) iff F = H/(x,y);

theorem :: ZF_LANG1:157
  H/(x,y) in WFF;

definition
  let H,x,y;
  redefine func H/(x,y) -> ZF-formula;
end;

theorem :: ZF_LANG1:158
  G1 '&' G2 = (H1 '&' H2)/(x,y) iff G1 = H1/(x,y) & G2 = H2/(x,y);

theorem :: ZF_LANG1:159
  z <> x implies (All(z,G) = All(z,H)/(x,y) iff G = H/(x,y));

theorem :: ZF_LANG1:160
  All(y,G) = All(x,H)/(x,y) iff G = H/(x,y);

theorem :: ZF_LANG1:161
  G1 'or' G2 = (H1 'or' H2)/(x,y) iff G1 = H1/(x,y) & G2 = H2/(x, y);

theorem :: ZF_LANG1:162
  G1 => G2 = (H1 => H2)/(x,y) iff G1 = H1/(x,y) & G2 = H2/(x,y);

theorem :: ZF_LANG1:163
  G1 <=> G2 = (H1 <=> H2)/(x,y) iff G1 = H1/(x,y) & G2 = H2/(x,y);

theorem :: ZF_LANG1:164
  z <> x implies (Ex(z,G) = Ex(z,H)/(x,y) iff G = H/(x,y));

theorem :: ZF_LANG1:165
  Ex(y,G) = Ex(x,H)/(x,y) iff G = H/(x,y);

theorem :: ZF_LANG1:166
  H is being_equality iff H/(x,y) is being_equality;

theorem :: ZF_LANG1:167
  H is being_membership iff H/(x,y) is being_membership;

theorem :: ZF_LANG1:168
  H is negative iff H/(x,y) is negative;

theorem :: ZF_LANG1:169
  H is conjunctive iff H/(x,y) is conjunctive;

theorem :: ZF_LANG1:170
  H is universal iff H/(x,y) is universal;

theorem :: ZF_LANG1:171
  H is negative implies the_argument_of (H/(x,y)) = (the_argument_of H)/
  (x, y );

theorem :: ZF_LANG1:172
  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:173
  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:174
  H is disjunctive iff H/(x,y) is disjunctive;

theorem :: ZF_LANG1:175
  H is conditional iff H/(x,y) is conditional;

theorem :: ZF_LANG1:176
  H is biconditional implies H/(x,y) is biconditional;

theorem :: ZF_LANG1:177
  H is existential iff H/(x,y) is existential;

theorem :: ZF_LANG1:178
  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:179
  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:180
  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:181
  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:182
  not x in variables_in H implies H/(x,y) = H;

theorem :: ZF_LANG1:183
  H/(x,x) = H;

theorem :: ZF_LANG1:184
  x <> y implies not x in variables_in (H/(x,y));

theorem :: ZF_LANG1:185
  x in variables_in H implies y in variables_in (H/(x,y));

theorem :: ZF_LANG1:186
  x <> y implies (H/(x,y))/(x,z) = H/(x,y);

theorem :: ZF_LANG1:187
  variables_in (H/(x,y)) c= (variables_in H \ {x}) \/ {y};