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

Metamath Proof Explorer

Theorem eqeltrdi

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

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

Proof

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