Metamath Proof Explorer

Theorem eleq1i

Description: Inference from equality to equivalence of membership. (Contributed by NM, 21-Jun-1993)

Ref Expression
Hypothesis eleq1i.1 
|- A = B
Assertion eleq1i 
|- ( A e. C <-> B e. C )

Proof

Step Hyp Ref Expression
1 eleq1i.1 
 |-  A = B
2 eleq1 
 |-  ( A = B -> ( A e. C <-> B e. C ) )
3 1 2 ax-mp 
 |-  ( A e. C <-> B e. C )