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

Metamath Proof Explorer

Theorem sbcel2gv

Description: Class substitution into a membership relation. (Contributed by NM, 17-Nov-2006) (Proof shortened by Andrew Salmon, 29-Jun-2011)

Ref Expression
Assertion sbcel2gv ⊢ B ∈ V → [˙B / x]˙ A ∈ x ↔ A ∈ B

Proof

Step Hyp Ref Expression
1 eleq2 ⊢ x = y → A ∈ x ↔ A ∈ y
2 eleq2 ⊢ y = B → A ∈ y ↔ A ∈ B
3 1 2 sbcie2g ⊢ B ∈ V → [˙B / x]˙ A ∈ x ↔ A ∈ B