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\in V\to \left(\underset{\dot{}}{[}B/x\underset{\dot{}}{]}A\in x\leftrightarrow A\in B\right)$$

Proof

Step	Hyp	Ref	Expression
1		eleq2	$$⊢x=y\to \left(A\in x\leftrightarrow A\in y\right)$$
2		eleq2	$$⊢y=B\to \left(A\in y\leftrightarrow A\in B\right)$$
3	1 2	sbcie2g	$$⊢B\in V\to \left(\underset{\dot{}}{[}B/x\underset{\dot{}}{]}A\in x\leftrightarrow A\in B\right)$$