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

Metamath Proof Explorer

Theorem eqeltrrid

Description: A membership and equality inference. (Contributed by NM, 4-Jan-2006)

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

Proof

Step Hyp Ref Expression
1 eqeltrrid.1 ⊢ B = A
2 eqeltrrid.2 ⊢ φ → B ∈ C
3 1 eqcomi ⊢ A = B
4 3 2 eqeltrid ⊢ φ → A ∈ C