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

Theorem pssnel 4199
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 4109 . . 3 (𝐴𝐵 → (𝐵𝐴) ≠ ∅)
2 n0 4095 . . 3 ((𝐵𝐴) ≠ ∅ ↔ ∃𝑥 𝑥 ∈ (𝐵𝐴))
31, 2sylib 209 . 2 (𝐴𝐵 → ∃𝑥 𝑥 ∈ (𝐵𝐴))
4 eldif 3742 . . 3 (𝑥 ∈ (𝐵𝐴) ↔ (𝑥𝐵 ∧ ¬ 𝑥𝐴))
54exbii 1943 . 2 (∃𝑥 𝑥 ∈ (𝐵𝐴) ↔ ∃𝑥(𝑥𝐵 ∧ ¬ 𝑥𝐴))
63, 5sylib 209 1 (𝐴𝐵 → ∃𝑥(𝑥𝐵 ∧ ¬ 𝑥𝐴))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 384  wex 1874  wcel 2155  wne 2937  cdif 3729  wpss 3733  c0 4079
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-v 3352  df-dif 3735  df-in 3739  df-ss 3746  df-pss 3748  df-nul 4080
This theorem is referenced by:  php  8351  php3  8353  pssnn  8385  inf3lem2  8741  infpssr  9383  ssfin4  9385  genpnnp  10080  ltexprlem1  10111  reclem2pr  10123  mrieqv2d  16567  lbspss  19354  lsmcv  19414  lidlnz  19502  obslbs  20350  nmoid  22825  spansncvi  28902  lsat0cv  34921  osumcllem11N  35854  pexmidlem8N  35865  isomenndlem  41316
  Copyright terms: Public domain W3C validator