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 e. V -> ( [. A / x ]. B e. C <-> [_ A / x ]_ B e. C ) )

Proof

Step	Hyp	Ref	Expression
1		sbcel12	|- ( [. A / x ]. B e. C <-> [_ A / x ]_ B e. [_ A / x ]_ C )
2		csbconstg	|- ( A e. V -> [_ A / x ]_ C = C )
3	2	eleq2d	|- ( A e. V -> ( [_ A / x ]_ B e. [_ A / x ]_ C <-> [_ A / x ]_ B e. C ) )
4	1 3	bitrid	|- ( A e. V -> ( [. A / x ]. B e. C <-> [_ A / x ]_ B e. C ) )