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

Theorem pssnel 4430
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 (𝐴𝐵 → ∃𝑥(𝑥𝐵 ∧ ¬ 𝑥𝐴))
Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

Proof of Theorem pssnel
StepHypRef Expression
1 pssdif 4326 . . 3 (𝐴𝐵 → (𝐵𝐴) ≠ ∅)
2 n0 4306 . . 3 ((𝐵𝐴) ≠ ∅ ↔ ∃𝑥 𝑥 ∈ (𝐵𝐴))
31, 2sylib 217 . 2 (𝐴𝐵 → ∃𝑥 𝑥 ∈ (𝐵𝐴))
4 eldif 3920 . . 3 (𝑥 ∈ (𝐵𝐴) ↔ (𝑥𝐵 ∧ ¬ 𝑥𝐴))
54exbii 1850 . 2 (∃𝑥 𝑥 ∈ (𝐵𝐴) ↔ ∃𝑥(𝑥𝐵 ∧ ¬ 𝑥𝐴))
63, 5sylib 217 1 (𝐴𝐵 → ∃𝑥(𝑥𝐵 ∧ ¬ 𝑥𝐴))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 396  wex 1781  wcel 2106  wne 2943  cdif 3907  wpss 3911  c0 4282
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2707
This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2714  df-cleq 2728  df-clel 2814  df-ne 2944  df-v 3447  df-dif 3913  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4283
This theorem is referenced by:  pssnn  9112  php  9154  php3  9156  phpOLD  9166  php3OLD  9168  pssnnOLD  9209  inf3lem2  9565  infpssr  10244  ssfin4  10246  genpnnp  10941  ltexprlem1  10972  reclem2pr  10984  mrieqv2d  17519  lbspss  20543  lsmcv  20602  lidlnz  20698  obslbs  21136  nmoid  24106  spansncvi  30594  fvineqsneq  35883  lsat0cv  37495  osumcllem11N  38429  pexmidlem8N  38440  isomenndlem  44761
  Copyright terms: Public domain W3C validator