Metamath Proof Explorer


Theorem eqeltri

Description: Substitution of equal classes into membership relation. (Contributed by NM, 21-Jun-1993)

Ref Expression
Hypotheses eqeltri.1
|- A = B
eqeltri.2
|- B e. C
Assertion eqeltri
|- A e. C

Proof

Step Hyp Ref Expression
1 eqeltri.1
 |-  A = B
2 eqeltri.2
 |-  B e. C
3 1 eleq1i
 |-  ( A e. C <-> B e. C )
4 2 3 mpbir
 |-  A e. C