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

Theorem pssnel 3881
Description: A proper subclass has a member in one argument that's not in both. (Contributed by NM, 29-Feb-1996.)
Assertion
Ref Expression
pssnel  |-  ( A 
C.  B  ->  E. x
( x  e.  B  /\  -.  x  e.  A
) )
Distinct variable groups:    x, A    x, B

Proof of Theorem pssnel
StepHypRef Expression
1 pssdif 3877 . . 3  |-  ( A 
C.  B  ->  ( B  \  A )  =/=  (/) )
2 n0 3793 . . 3  |-  ( ( B  \  A )  =/=  (/)  <->  E. x  x  e.  ( B  \  A
) )
31, 2sylib 196 . 2  |-  ( A 
C.  B  ->  E. x  x  e.  ( B  \  A ) )
4 eldif 3471 . . 3  |-  ( x  e.  ( B  \  A )  <->  ( x  e.  B  /\  -.  x  e.  A ) )
54exbii 1672 . 2  |-  ( E. x  x  e.  ( B  \  A )  <->  E. x ( x  e.  B  /\  -.  x  e.  A ) )
63, 5sylib 196 1  |-  ( A 
C.  B  ->  E. x
( x  e.  B  /\  -.  x  e.  A
) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 367   E.wex 1617    e. wcel 1823    =/= wne 2649    \ cdif 3458    C. wpss 3462   (/)c0 3783
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2651  df-v 3108  df-dif 3464  df-in 3468  df-ss 3475  df-pss 3477  df-nul 3784
This theorem is referenced by:  php  7694  php3  7696  pssnn  7731  inf3lem2  8037  infpssr  8679  ssfin4  8681  genpnnp  9372  ltexprlem1  9403  reclem2pr  9415  mrieqv2d  15131  lbspss  17926  lsmcv  17985  lidlnz  18074  obslbs  18937  nmoid  21418  spansncvi  26771  lsat0cv  35174  osumcllem11N  36106  pexmidlem8N  36117
  Copyright terms: Public domain W3C validator