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	⊢ ( 𝐵 ∈ 𝑉 → ( [ 𝐵 / 𝑥 ] 𝐴 ∈ 𝑥 ↔ 𝐴 ∈ 𝐵 ) )

Step	Hyp	Ref	Expression
1		eleq2	⊢ ( 𝑥 = 𝑦 → ( 𝐴 ∈ 𝑥 ↔ 𝐴 ∈ 𝑦 ) )
2		eleq2	⊢ ( 𝑦 = 𝐵 → ( 𝐴 ∈ 𝑦 ↔ 𝐴 ∈ 𝐵 ) )
3	1 2	sbcie2g	⊢ ( 𝐵 ∈ 𝑉 → ( [ 𝐵 / 𝑥 ] 𝐴 ∈ 𝑥 ↔ 𝐴 ∈ 𝐵 ) )