Theorem sbcel1g

Description: Move proper substitution in and out of a membership relation. Note that the scope of [. A / x ]. is the wff B e. C , whereas the scope of [_ A / x ]_ is the class B . (Contributed by NM, 10-Nov-2005)

	Ref	Expression
Assertion	sbcel1g	$$⊢A\in V\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}B\in C\leftrightarrow ⦋A/x⦌B\in C\right)$$

Proof

Step	Hyp	Ref	Expression
1		sbcel12	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}B\in C\leftrightarrow ⦋A/x⦌B\in ⦋A/x⦌C$$
2		csbconstg	$$⊢A\in V\to ⦋A/x⦌C=C$$
3	2	eleq2d	$$⊢A\in V\to \left(⦋A/x⦌B\in ⦋A/x⦌C\leftrightarrow ⦋A/x⦌B\in C\right)$$
4	1 3	bitrid	$$⊢A\in V\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}B\in C\leftrightarrow ⦋A/x⦌B\in C\right)$$