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

Theorem pssnel 3843
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 3839 . . 3  |-  ( A 
C.  B  ->  ( B  \  A )  =/=  (/) )
2 n0 3752 . . 3  |-  ( ( B  \  A )  =/=  (/)  <->  E. x  x  e.  ( B  \  A
) )
31, 2sylib 201 . 2  |-  ( A 
C.  B  ->  E. x  x  e.  ( B  \  A ) )
4 eldif 3425 . . 3  |-  ( x  e.  ( B  \  A )  <->  ( x  e.  B  /\  -.  x  e.  A ) )
54exbii 1728 . 2  |-  ( E. x  x  e.  ( B  \  A )  <->  E. x ( x  e.  B  /\  -.  x  e.  A ) )
63, 5sylib 201 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 375   E.wex 1673    e. wcel 1897    =/= wne 2632    \ cdif 3412    C. wpss 3416   (/)c0 3742
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-10 1925  ax-11 1930  ax-12 1943  ax-13 2101  ax-ext 2441
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-tru 1457  df-ex 1674  df-nf 1678  df-sb 1808  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2591  df-ne 2634  df-v 3058  df-dif 3418  df-in 3422  df-ss 3429  df-pss 3431  df-nul 3743
This theorem is referenced by:  php  7781  php3  7783  pssnn  7815  inf3lem2  8159  infpssr  8763  ssfin4  8765  genpnnp  9455  ltexprlem1  9486  reclem2pr  9498  mrieqv2d  15593  lbspss  18353  lsmcv  18412  lidlnz  18500  obslbs  19341  nmoid  21811  spansncvi  27353  lsat0cv  32643  osumcllem11N  33575  pexmidlem8N  33586  isomenndlem  38388
  Copyright terms: Public domain W3C validator