Metamath Proof Explorer

Theorem elequ2

Description: An identity law for the non-logical predicate. (Contributed by NM, 21-Jun-1993)

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

Proof

Step Hyp Ref Expression
1 ax9 
 |-  ( x = y -> ( z e. x -> z e. y ) )
2 ax9 
 |-  ( y = x -> ( z e. y -> z e. x ) )
3 2 equcoms 
 |-  ( x = y -> ( z e. y -> z e. x ) )
4 1 3 impbid 
 |-  ( x = y -> ( z e. x <-> z e. y ) )