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, Th173, Th174;
hence H / x,y is universal by ZF_LANG:16; :: thesis: verum

end;

assume A3: H / x,y is universal ; :: thesis: H is universal
( 1 <= 3 & 3 <= len H ) by ZF_LANG:29;
then ( 1 <= 1 & 1 <= len H ) by XXREAL_0:2;
then A4: ( (H / x,y) . 1 = 4 & y <> 4 & 1 in dom H ) by A3, Th148, FINSEQ_3:27, ZF_LANG:39;
then H . 1 <> x by Def4;
then 4 = H . 1 by A4, Def4;
hence H is universal by ZF_LANG:45; :: thesis: verum