Metamath Proof Explorer

Theorem nssrex

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

Ref Expression
Assertion nssrex 
|- ( -. A C_ B <-> E. x e. A -. x e. B )

Proof

Step Hyp Ref Expression
1 nss 
 |-  ( -. A C_ B <-> E. x ( x e. A /\ -. x e. B ) )
2 df-rex 
 |-  ( E. x e. A -. x e. B <-> E. x ( x e. A /\ -. x e. B ) )
3 1 2 bitr4i 
 |-  ( -. A C_ B <-> E. x e. A -. x e. B )