MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  nss Unicode version

Theorem nss 3342
Description: Negation of subclass relationship. Exercise 13 of [TakeutiZaring] p. 18. (Contributed by NM, 25-Feb-1996.) (Proof shortened by Andrew Salmon, 21-Jun-2011.)
Assertion
Ref Expression
nss  |-  ( -.  A  C_  B  <->  E. x
( x  e.  A  /\  -.  x  e.  B
) )
Distinct variable groups:    x, A    x, B

Proof of Theorem nss
StepHypRef Expression
1 exanali 1592 . . 3  |-  ( E. x ( x  e.  A  /\  -.  x  e.  B )  <->  -.  A. x
( x  e.  A  ->  x  e.  B ) )
2 dfss2 3273 . . 3  |-  ( A 
C_  B  <->  A. x
( x  e.  A  ->  x  e.  B ) )
31, 2xchbinxr 303 . 2  |-  ( E. x ( x  e.  A  /\  -.  x  e.  B )  <->  -.  A  C_  B )
43bicomi 194 1  |-  ( -.  A  C_  B  <->  E. x
( x  e.  A  /\  -.  x  e.  B
) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 177    /\ wa 359   A.wal 1546   E.wex 1547    e. wcel 1717    C_ wss 3256
This theorem is referenced by:  grur1  8621  psslinpr  8834  reclem2pr  8851  mreexexlem2d  13790  prmcyg  15423  filcon  17829  alexsubALTlem4  17995  wilthlem2  20712  shne0i  22791  erdszelem10  24658  fundmpss  25139
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2361
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2367  df-cleq 2373  df-clel 2376  df-in 3263  df-ss 3270
  Copyright terms: Public domain W3C validator