Theorem nssd

Description: Negation of subclass relationship. (Contributed by Glauco Siliprandi, 26-Jun-2021)

	Ref	Expression
Hypotheses	nssd.1	$$⊢\phi \to X\in A$$
	nssd.2	$$⊢\phi \to \neg X\in B$$
Assertion	nssd	$$⊢\phi \to \neg A\subseteq B$$

Proof

Step	Hyp	Ref	Expression
1		nssd.1	$$⊢\phi \to X\in A$$
2		nssd.2	$$⊢\phi \to \neg X\in B$$
3	1 2	jca	$$⊢\phi \to \left(X\in A\wedge \neg X\in B\right)$$
4		eleq1	$$⊢x=X\to \left(x\in A\leftrightarrow X\in A\right)$$
5		eleq1	$$⊢x=X\to \left(x\in B\leftrightarrow X\in B\right)$$
6	5	notbid	$$⊢x=X\to \left(\neg x\in B\leftrightarrow \neg X\in B\right)$$
7	4 6	anbi12d	$$⊢x=X\to \left(\left(x\in A\wedge \neg x\in B\right)\leftrightarrow \left(X\in A\wedge \neg X\in B\right)\right)$$
8	7	spcegv	$$⊢X\in A\to \left(\left(X\in A\wedge \neg X\in B\right)\to \exists x\left(x\in A\wedge \neg x\in B\right)\right)$$
9	1 3 8	sylc	$$⊢\phi \to \exists x\left(x\in A\wedge \neg x\in B\right)$$
10		nss	$$⊢\neg A\subseteq B\leftrightarrow \exists x\left(x\in A\wedge \neg x\in B\right)$$
11	9 10	sylibr	$$⊢\phi \to \neg A\subseteq B$$