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

Metamath Proof Explorer

Theorem eqeltrid

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

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

Proof

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