Metamath Proof Explorer

Theorem elequ1

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

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

Proof

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