This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem eqeltrrd

Description: Deduction that substitutes equal classes into membership. (Contributed by NM, 14-Dec-2004)

Ref Expression
Hypotheses eqeltrrd.1 ⊢ φ → A = B
eqeltrrd.2 ⊢ φ → A ∈ C
Assertion eqeltrrd ⊢ φ → B ∈ C

Proof

Step Hyp Ref Expression
1 eqeltrrd.1 ⊢ φ → A = B
2 eqeltrrd.2 ⊢ φ → A ∈ C
3 1 eqcomd ⊢ φ → B = A
4 3 2 eqeltrd ⊢ φ → B ∈ C