Theorem rspcsbnea

Description: Special case related to rspsbc . (Contributed by metakunt, 5-May-2025)

	Ref	Expression
Assertion	rspcsbnea	$$⊢\left(A\in B\wedge \forall x\in BC\ne D\right)\to ⦋A/x⦌C\ne D$$

Proof

Step	Hyp	Ref	Expression
1		rspsbc	$$⊢A\in B\to \left(\forall x\in BC\ne D\to \underset{\dot{}}{[}A/x\underset{\dot{}}{]}C\ne D\right)$$
2		df-ne	$$⊢C\ne D\leftrightarrow \neg C=D$$
3	2	sbcbii	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}C\ne D\leftrightarrow \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\neg C=D$$
4	3	a1i	$$⊢A\in B\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}C\ne D\leftrightarrow \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\neg C=D\right)$$
5		sbcng	$$⊢A\in B\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\neg C=D\leftrightarrow \neg \underset{\dot{}}{[}A/x\underset{\dot{}}{]}C=D\right)$$
6		sbceq1g	$$⊢A\in B\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}C=D\leftrightarrow ⦋A/x⦌C=D\right)$$
7	6	notbid	$$⊢A\in B\to \left(\neg \underset{\dot{}}{[}A/x\underset{\dot{}}{]}C=D\leftrightarrow \neg ⦋A/x⦌C=D\right)$$
8	5 7	bitrd	$$⊢A\in B\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\neg C=D\leftrightarrow \neg ⦋A/x⦌C=D\right)$$
9	4 8	bitrd	$$⊢A\in B\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}C\ne D\leftrightarrow \neg ⦋A/x⦌C=D\right)$$
10		biidd	$$⊢A\in B\to \left(⦋A/x⦌C=D\leftrightarrow ⦋A/x⦌C=D\right)$$
11	10	necon3bbid	$$⊢A\in B\to \left(\neg ⦋A/x⦌C=D\leftrightarrow ⦋A/x⦌C\ne D\right)$$
12	9 11	bitrd	$$⊢A\in B\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}C\ne D\leftrightarrow ⦋A/x⦌C\ne D\right)$$
13	1 12	sylibd	$$⊢A\in B\to \left(\forall x\in BC\ne D\to ⦋A/x⦌C\ne D\right)$$
14	13	imp	$$⊢\left(A\in B\wedge \forall x\in BC\ne D\right)\to ⦋A/x⦌C\ne D$$