Metamath Proof Explorer

Theorem eleq1a

Description: A transitive-type law relating membership and equality. (Contributed by NM, 9-Apr-1994)

Ref Expression
Assertion eleq1a 
|- ( A e. B -> ( C = A -> C e. B ) )

Proof

Step Hyp Ref Expression
1 eleq1 
 |-  ( C = A -> ( C e. B <-> A e. B ) )
2 1 biimprcd 
 |-  ( A e. B -> ( C = A -> C e. B ) )