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

Theorem pssnel 4471
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 4367 . . 3 (𝐴𝐵 → (𝐵𝐴) ≠ ∅)
2 n0 4347 . . 3 ((𝐵𝐴) ≠ ∅ ↔ ∃𝑥 𝑥 ∈ (𝐵𝐴))
31, 2sylib 217 . 2 (𝐴𝐵 → ∃𝑥 𝑥 ∈ (𝐵𝐴))
4 eldif 3959 . . 3 (𝑥 ∈ (𝐵𝐴) ↔ (𝑥𝐵 ∧ ¬ 𝑥𝐴))
54exbii 1851 . 2 (∃𝑥 𝑥 ∈ (𝐵𝐴) ↔ ∃𝑥(𝑥𝐵 ∧ ¬ 𝑥𝐴))
63, 5sylib 217 1 (𝐴𝐵 → ∃𝑥(𝑥𝐵 ∧ ¬ 𝑥𝐴))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 397  wex 1782  wcel 2107  wne 2941  cdif 3946  wpss 3950  c0 4323
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ne 2942  df-v 3477  df-dif 3952  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4324
This theorem is referenced by:  pssnn  9168  php  9210  php3  9212  phpOLD  9222  php3OLD  9224  pssnnOLD  9265  inf3lem2  9624  infpssr  10303  ssfin4  10305  genpnnp  11000  ltexprlem1  11031  reclem2pr  11043  mrieqv2d  17583  lbspss  20693  lsmcv  20754  lidlnz  20853  obslbs  21285  nmoid  24259  spansncvi  30905  fvineqsneq  36293  lsat0cv  37903  osumcllem11N  38837  pexmidlem8N  38848  isomenndlem  45246
  Copyright terms: Public domain W3C validator