This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )