Metamath Proof Explorer

Theorem elequ2g

Description: A form of elequ2 with a universal quantifier. Its converse is the axiom of extensionality ax-ext . (Contributed by BJ, 3-Oct-2019)

Ref Expression
Assertion elequ2g 
|- ( x = y -> A. z ( z e. x <-> z e. y ) )

Proof

Step Hyp Ref Expression
1 elequ2 
 |-  ( x = y -> ( z e. x <-> z e. y ) )
2 1 alrimiv 
 |-  ( x = y -> A. z ( z e. x <-> z e. y ) )