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

Metamath Proof Explorer

Theorem eleq2s

Description: Substitution of equal classes into a membership antecedent. (Contributed by Jonathan Ben-Naim, 3-Jun-2011)

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

Proof

Step Hyp Ref Expression
1 eleq2s.1 ⊢ A ∈ B → φ
2 eleq2s.2 ⊢ C = B
3 2 eleq2i ⊢ A ∈ C ↔ A ∈ B
4 3 1 sylbi ⊢ A ∈ C → φ