Metamath Proof Explorer
Description: Substitution of equal classes into membership relation. (Contributed by NM, 21Jun1993)


Ref 
Expression 

Hypotheses 
eqeltri.1 
$${\u22a2}{A}={B}$$ 


eqeltri.2 
$${\u22a2}{B}\in {C}$$ 

Assertion 
eqeltri 
$${\u22a2}{A}\in {C}$$ 
Proof
Step 
Hyp 
Ref 
Expression 
1 

eqeltri.1 
$${\u22a2}{A}={B}$$ 
2 

eqeltri.2 
$${\u22a2}{B}\in {C}$$ 
3 
1

eleq1i 
$${\u22a2}{A}\in {C}\leftrightarrow {B}\in {C}$$ 
4 
2 3

mpbir 
$${\u22a2}{A}\in {C}$$ 