Theorem sbcnel12g

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

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

Proof

Step	Hyp	Ref	Expression
1		sbcng	$$⊢A\in V\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\neg B\in C\leftrightarrow \neg \underset{\dot{}}{[}A/x\underset{\dot{}}{]}B\in C\right)$$
2		df-nel	$$⊢B\notin C\leftrightarrow \neg B\in C$$
3	2	sbcbii	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}B\notin C\leftrightarrow \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\neg B\in C$$
4		df-nel	$$⊢⦋A/x⦌B\notin ⦋A/x⦌C\leftrightarrow \neg ⦋A/x⦌B\in ⦋A/x⦌C$$
5		sbcel12	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}B\in C\leftrightarrow ⦋A/x⦌B\in ⦋A/x⦌C$$
6	4 5	xchbinxr	$$⊢⦋A/x⦌B\notin ⦋A/x⦌C\leftrightarrow \neg \underset{\dot{}}{[}A/x\underset{\dot{}}{]}B\in C$$
7	1 3 6	3bitr4g	$$⊢A\in V\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}B\notin C\leftrightarrow ⦋A/x⦌B\notin ⦋A/x⦌C\right)$$