Metamath Proof Explorer

Theorem eqeltr

Description: Substitution of equal classes into element relation. (Contributed by Peter Mazsa, 22-Jul-2017)

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

Proof

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