let H be ZF-formula; :: thesis: for x, y being Variable holds
( H is universal iff H / (x,y) is universal )
let x, y be Variable; :: thesis: ( H is universal iff H / (x,y) is universal )
thus ( H is universal implies H / (x,y) is universal ) :: thesis: ( H / (x,y) is universal implies H is universal )
proof
given z being Variable, H1 being ZF-formula such that A1: H = All (z,H1) ; :: according to ZF_LANG:def 14 :: thesis: H / (x,y) is universal
( z = x or z <> x ) ;
then consider s being Variable such that
A2: ( ( z = x & s = y ) or ( z <> x & s = z ) ) ;
H / (x,y) = All (s,(H1 / (x,y))) by A1, A2, Th159, Th160;
hence H / (x,y) is universal ; :: thesis: verum
end;
assume H / (x,y) is universal ; :: thesis: H is universal
then A3: (H / (x,y)) . 1 = 4 by ZF_LANG:22;
3 <= len H by ZF_LANG:13;
then 1 <= len H by XXREAL_0:2;
then A4: 1 in dom H by FINSEQ_3:25;
y <> 4 by Th135;
then H . 1 <> x by A3, A4, Def3;
then 4 = H . 1 by A3, A4, Def3;
hence H is universal by ZF_LANG:28; :: thesis: verum