Metamath Proof Explorer
Description: Deduction that substitutes equal classes into membership. (Contributed by NM, 14Dec2004)


Ref 
Expression 

Hypotheses 
eleqtrd.1 
⊢ ( 𝜑 → 𝐴 ∈ 𝐵 ) 


eleqtrd.2 
⊢ ( 𝜑 → 𝐵 = 𝐶 ) 

Assertion 
eleqtrd 
⊢ ( 𝜑 → 𝐴 ∈ 𝐶 ) 
Proof
Step 
Hyp 
Ref 
Expression 
1 

eleqtrd.1 
⊢ ( 𝜑 → 𝐴 ∈ 𝐵 ) 
2 

eleqtrd.2 
⊢ ( 𝜑 → 𝐵 = 𝐶 ) 
3 
2

eleq2d 
⊢ ( 𝜑 → ( 𝐴 ∈ 𝐵 ↔ 𝐴 ∈ 𝐶 ) ) 
4 
1 3

mpbid 
⊢ ( 𝜑 → 𝐴 ∈ 𝐶 ) 