Theorem sbcnel12g

Description: Distribute proper substitution through negated membership. (Contributed by Andrew Salmon, 18-Jun-2011)

	Ref	Expression
Assertion	sbcnel12g	|- ( A e. V -> ( [. A / x ]. B e/ C <-> [_ A / x ]_ B e/ [_ A / x ]_ C ) )

Proof

Step	Hyp	Ref	Expression
1		sbcng	|- ( A e. V -> ( [. A / x ]. -. B e. C <-> -. [. A / x ]. B e. C ) )
2		df-nel	|- ( B e/ C <-> -. B e. C )
3	2	sbcbii	|- ( [. A / x ]. B e/ C <-> [. A / x ]. -. B e. C )
4		df-nel	|- ( [_ A / x ]_ B e/ [_ A / x ]_ C <-> -. [_ A / x ]_ B e. [_ A / x ]_ C )
5		sbcel12	|- ( [. A / x ]. B e. C <-> [_ A / x ]_ B e. [_ A / x ]_ C )
6	4 5	xchbinxr	|- ( [_ A / x ]_ B e/ [_ A / x ]_ C <-> -. [. A / x ]. B e. C )
7	1 3 6	3bitr4g	|- ( A e. V -> ( [. A / x ]. B e/ C <-> [_ A / x ]_ B e/ [_ A / x ]_ C ) )