let p1, p2 be ZF-formula; :: thesis: for x1, y1, x2, y2 being Variable st All x1,y1,p1 = All x2,y2,p2 holds
( x1 = x2 & y1 = y2 & p1 = p2 )
let x1, y1, x2, y2 be Variable; :: thesis: ( All x1,y1,p1 = All x2,y2,p2 implies ( x1 = x2 & y1 = y2 & p1 = p2 ) )
assume All x1,y1,p1 = All x2,y2,p2 ; :: thesis: ( x1 = x2 & y1 = y2 & p1 = p2 )
then ( x1 = x2 & All y1,p1 = All y2,p2 ) by ZF_LANG:12;
hence ( x1 = x2 & y1 = y2 & p1 = p2 ) by ZF_LANG:12; :: thesis: verum