let E be non empty set ; :: thesis: for x being Variable
for H being ZF-formula
for f being Function of VAR,E holds
( ( f in St (H,E) & ( for g being Function of VAR,E st ( for y being Variable st g . y <> f . y holds
x = y ) holds
g in St (H,E) ) ) iff f in St ((All (x,H)),E) )
let x be Variable; :: thesis: for H being ZF-formula
for f being Function of VAR,E holds
( ( f in St (H,E) & ( for g being Function of VAR,E st ( for y being Variable st g . y <> f . y holds
x = y ) holds
g in St (H,E) ) ) iff f in St ((All (x,H)),E) )
let H be ZF-formula; :: thesis: for f being Function of VAR,E holds
( ( f in St (H,E) & ( for g being Function of VAR,E st ( for y being Variable st g . y <> f . y holds
x = y ) holds
g in St (H,E) ) ) iff f in St ((All (x,H)),E) )
let f be Function of VAR,E; :: thesis: ( ( f in St (H,E) & ( for g being Function of VAR,E st ( for y being Variable st g . y <> f . y holds
x = y ) holds
g in St (H,E) ) ) iff f in St ((All (x,H)),E) )
A1: All (x,H) is universal ;
then A2: St ((All (x,H)),E) = { v5 where v5 is Element of VAL E : for X being set
for f being Function of VAR,E st X = St ((the_scope_of (All (x,H))),E) & 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 (All (x,H)) = y ) holds
g in X ) ) } by Lm3;
A3: All (x,H) = All ((bound_in (All (x,H))),(the_scope_of (All (x,H)))) by A1, ZF_LANG:44;
then A4: x = bound_in (All (x,H)) by ZF_LANG:3;
A5: H = the_scope_of (All (x,H)) by A3, ZF_LANG:3;
thus ( f in St (H,E) & ( for g being Function of VAR,E st ( for y being Variable st g . y <> f . y holds
x = y ) holds
g in St (H,E) ) implies f in St ((All (x,H)),E) ) :: thesis: ( f in St ((All (x,H)),E) implies ( f in St (H,E) & ( for g being Function of VAR,E st ( for y being Variable st g . y <> f . y holds
x = y ) holds
g in St (H,E) ) ) )

proof

reconsider v = f as Element of VAL E by FUNCT_2:8;
assume ( f in St (H,E) & ( for g being Function of VAR,E st ( for y being Variable st g . y <> f . y holds
x = y ) holds
g in St (H,E) ) ) ; :: thesis: f in St ((All (x,H)),E)
then for X being set
for h being Function of VAR,E st X = St ((the_scope_of (All (x,H))),E) & h = v holds
( h in X & ( for g being Function of VAR,E st ( for y being Variable st g . y <> h . y holds
bound_in (All (x,H)) = y ) holds
g in X ) ) by A4, A5;
hence f in St ((All (x,H)),E) by A2; :: thesis: verum

end;

assume f in St ((All (x,H)),E) ; :: thesis: ( f in St (H,E) & ( for g being Function of VAR,E st ( for y being Variable st g . y <> f . y holds
x = y ) holds
g in St (H,E) ) )
then A6: ex v5 being Element of VAL E st
( f = v5 & ( for X being set
for f being Function of VAR,E st X = St ((the_scope_of (All (x,H))),E) & 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 (All (x,H)) = y ) holds
g in X ) ) ) ) by A2;
hence f in St (H,E) by A5; :: thesis: for g being Function of VAR,E st ( for y being Variable st g . y <> f . y holds
x = y ) holds
g in St (H,E)
let g be Function of VAR,E; :: thesis: ( ( for y being Variable st g . y <> f . y holds
x = y ) implies g in St (H,E) )
assume for y being Variable st g . y <> f . y holds
x = y ; :: thesis: g in St (H,E)
hence g in St (H,E) by A4, A5, A6; :: thesis: verum