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


Ref 
Expression 

Hypotheses 
eqeltrrd.1 
 ( ph > A = B ) 


eqeltrrd.2 
 ( ph > A e. C ) 

Assertion 
eqeltrrd 
 ( ph > B e. C ) 
Proof
Step 
Hyp 
Ref 
Expression 
1 

eqeltrrd.1 
 ( ph > A = B ) 
2 

eqeltrrd.2 
 ( ph > A e. C ) 
3 
1

eqcomd 
 ( ph > B = A ) 
4 
3 2

eqeltrd 
 ( ph > B e. C ) 