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

Theorem pssnel 3839
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 3836 . . 3  |-  ( A 
C.  B  ->  ( B  \  A )  =/=  (/) )
2 n0 3741 . . 3  |-  ( ( B  \  A )  =/=  (/)  <->  E. x  x  e.  ( B  \  A
) )
31, 2sylib 196 . 2  |-  ( A 
C.  B  ->  E. x  x  e.  ( B  \  A ) )
4 eldif 3433 . . 3  |-  ( x  e.  ( B  \  A )  <->  ( x  e.  B  /\  -.  x  e.  A ) )
54exbii 1635 . 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 369   E.wex 1587    e. wcel 1758    =/= wne 2642    \ cdif 3420    C. wpss 3424   (/)c0 3732
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2599  df-ne 2644  df-v 3067  df-dif 3426  df-in 3430  df-ss 3437  df-pss 3439  df-nul 3733
This theorem is referenced by:  php  7592  php3  7594  pssnn  7629  inf3lem2  7933  infpssr  8575  ssfin4  8577  genpnnp  9272  ltexprlem1  9303  reclem2pr  9315  mrieqv2d  14676  lbspss  17266  lsmcv  17325  lidlnz  17413  obslbs  18261  nmoid  20434  spansncvi  25187  lsat0cv  32981  osumcllem11N  33913  pexmidlem8N  33924
  Copyright terms: Public domain W3C validator