Metamath Proof Explorer

Theorem eleq12

Description: Equality implies equivalence of membership. (Contributed by NM, 31-May-1999)

Ref Expression
Assertion eleq12 
|- ( ( A = B /\ C = D ) -> ( A e. C <-> B e. D ) )

Proof

Step Hyp Ref Expression
1 eleq1 
 |-  ( A = B -> ( A e. C <-> B e. C ) )
2 eleq2 
 |-  ( C = D -> ( B e. C <-> B e. D ) )
3 1 2 sylan9bb 
 |-  ( ( A = B /\ C = D ) -> ( A e. C <-> B e. D ) )