let a1, a2 be set ; :: thesis: ( ex A being set st
( ( for x, y being Variable holds
( [(x '=' y),{ v1 where v1 is Element of VAL E : for f being Function of VAR ,E st f = v1 holds
f . x = f . y } ] in A & [(x 'in' y),{ v2 where v2 is Element of VAL E : for f being Function of VAR ,E st f = v2 holds
f . x in f . y } ] in A ) ) & [H,a1] in A & ( for H' being ZF-formula
for a being set st [H',a] in A holds
( ( H' is being_equality implies a = { v3 where v3 is Element of VAL E : for f being Function of VAR ,E st f = v3 holds
f . (Var1 H') = f . (Var2 H') } ) & ( H' is being_membership implies a = { v4 where v4 is Element of VAL E : for f being Function of VAR ,E st f = v4 holds
f . (Var1 H') in f . (Var2 H') } ) & ( H' is negative implies ex b being set st
( a = (VAL E) \ (union {b}) & [(the_argument_of H'),b] in A ) ) & ( H' is conjunctive implies ex b, c being set st
( a = (union {b}) /\ (union {c}) & [(the_left_argument_of H'),b] in A & [(the_right_argument_of H'),c] in A ) ) & ( H' is universal implies ex b being set st
( a = { v5 where v5 is Element of VAL E : for X being set
for f being Function of VAR ,E st X = b & f = v5 holds
( f in X & ( for g being Function of VAR ,E st ( for y being Variable st g . y <> f . y holds
bound_in H' = y ) holds
g in X ) ) } & [(the_scope_of H'),b] in A ) ) ) ) ) & ex A being set st
( ( for x, y being Variable holds
( [(x '=' y),{ v1 where v1 is Element of VAL E : for f being Function of VAR ,E st f = v1 holds
f . x = f . y } ] in A & [(x 'in' y),{ v2 where v2 is Element of VAL E : for f being Function of VAR ,E st f = v2 holds
f . x in f . y } ] in A ) ) & [H,a2] in A & ( for H' being ZF-formula
for a being set st [H',a] in A holds
( ( H' is being_equality implies a = { v3 where v3 is Element of VAL E : for f being Function of VAR ,E st f = v3 holds
f . (Var1 H') = f . (Var2 H') } ) & ( H' is being_membership implies a = { v4 where v4 is Element of VAL E : for f being Function of VAR ,E st f = v4 holds
f . (Var1 H') in f . (Var2 H') } ) & ( H' is negative implies ex b being set st
( a = (VAL E) \ (union {b}) & [(the_argument_of H'),b] in A ) ) & ( H' is conjunctive implies ex b, c being set st
( a = (union {b}) /\ (union {c}) & [(the_left_argument_of H'),b] in A & [(the_right_argument_of H'),c] in A ) ) & ( H' is universal implies ex b being set st
( a = { v5 where v5 is Element of VAL E : for X being set
for f being Function of VAR ,E st X = b & f = v5 holds
( f in X & ( for g being Function of VAR ,E st ( for y being Variable st g . y <> f . y holds
bound_in H' = y ) holds
g in X ) ) } & [(the_scope_of H'),b] in A ) ) ) ) ) implies a1 = a2 )
assume that
A1: ex A being set st
( ( for x, y being Variable holds
( [(x '=' y),H₇(x,y)] in A & [(x 'in' y),H₈(x,y)] in A ) ) & [H,a1] in A & ( for H' being ZF-formula
for a being set st [H',a] in A holds
( ( H' is being_equality implies a = H₇( Var1 H', Var2 H') ) & ( H' is being_membership implies a = H₈( Var1 H', Var2 H') ) & ( H' is negative implies ex b being set st
( a = H₉(b) & [(the_argument_of H'),b] in A ) ) & ( H' is conjunctive implies ex b, c being set st
( a = H₁₀(b,c) & [(the_left_argument_of H'),b] in A & [(the_right_argument_of H'),c] in A ) ) & ( H' is universal implies ex b being set st
( a = H₁₁( bound_in H',b) & [(the_scope_of H'),b] in A ) ) ) ) ) and
A2: ex A being set st
( ( for x, y being Variable holds
( [(x '=' y),H₇(x,y)] in A & [(x 'in' y),H₈(x,y)] in A ) ) & [H,a2] in A & ( for H' being ZF-formula
for a being set st [H',a] in A holds
( ( H' is being_equality implies a = H₇( Var1 H', Var2 H') ) & ( H' is being_membership implies a = H₈( Var1 H', Var2 H') ) & ( H' is negative implies ex b being set st
( a = H₉(b) & [(the_argument_of H'),b] in A ) ) & ( H' is conjunctive implies ex b, c being set st
( a = H₁₀(b,c) & [(the_left_argument_of H'),b] in A & [(the_right_argument_of H'),c] in A ) ) & ( H' is universal implies ex b being set st
( a = H₁₁( bound_in H',b) & [(the_scope_of H'),b] in A ) ) ) ) ) ; :: thesis: a1 = a2
thus a1 = a2 from ZF_MODEL:sch 2(A1, A2); :: thesis: verum