Theorem nssd

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

	Ref	Expression
Hypotheses	nssd.1	|- ( ph -> X e. A )
	nssd.2	|- ( ph -> -. X e. B )
Assertion	nssd	|- ( ph -> -. A C_ B )

Proof

Step	Hyp	Ref	Expression
1		nssd.1	|- ( ph -> X e. A )
2		nssd.2	|- ( ph -> -. X e. B )
3	1 2	jca	|- ( ph -> ( X e. A /\ -. X e. B ) )
4		eleq1	|- ( x = X -> ( x e. A <-> X e. A ) )
5		eleq1	|- ( x = X -> ( x e. B <-> X e. B ) )
6	5	notbid	|- ( x = X -> ( -. x e. B <-> -. X e. B ) )
7	4 6	anbi12d	|- ( x = X -> ( ( x e. A /\ -. x e. B ) <-> ( X e. A /\ -. X e. B ) ) )
8	7	spcegv	|- ( X e. A -> ( ( X e. A /\ -. X e. B ) -> E. x ( x e. A /\ -. x e. B ) ) )
9	1 3 8	sylc	|- ( ph -> E. x ( x e. A /\ -. x e. B ) )
10		nss	|- ( -. A C_ B <-> E. x ( x e. A /\ -. x e. B ) )
11	9 10	sylibr	|- ( ph -> -. A C_ B )