let p, q be ZF-formula; :: thesis: for x, y, z, t, s being Variable st All x,y,z,p = All t,s,q holds
( x = t & y = s & All z,p = q )
let x, y, z, t, s be Variable; :: thesis: ( All x,y,z,p = All t,s,q implies ( x = t & y = s & All z,p = q ) )
All x,y,z,p = All x,y,(All z,p) ;
hence ( All x,y,z,p = All t,s,q implies ( x = t & y = s & All z,p = q ) ) by Th16; :: thesis: verum