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

Theorem pssnel 4367
 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 4265 . . 3 (𝐴𝐵 → (𝐵𝐴) ≠ ∅)
2 n0 4245 . . 3 ((𝐵𝐴) ≠ ∅ ↔ ∃𝑥 𝑥 ∈ (𝐵𝐴))
31, 2sylib 221 . 2 (𝐴𝐵 → ∃𝑥 𝑥 ∈ (𝐵𝐴))
4 eldif 3868 . . 3 (𝑥 ∈ (𝐵𝐴) ↔ (𝑥𝐵 ∧ ¬ 𝑥𝐴))
54exbii 1849 . 2 (∃𝑥 𝑥 ∈ (𝐵𝐴) ↔ ∃𝑥(𝑥𝐵 ∧ ¬ 𝑥𝐴))
63, 5sylib 221 1 (𝐴𝐵 → ∃𝑥(𝑥𝐵 ∧ ¬ 𝑥𝐴))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 399  ∃wex 1781   ∈ wcel 2111   ≠ wne 2951   ∖ cdif 3855   ⊊ wpss 3859  ∅c0 4225 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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2729 This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1541  df-fal 1551  df-ex 1782  df-sb 2070  df-clab 2736  df-cleq 2750  df-clel 2830  df-ne 2952  df-v 3411  df-dif 3861  df-in 3865  df-ss 3875  df-pss 3877  df-nul 4226 This theorem is referenced by:  php  8723  php3  8725  pssnn  8738  pssnnOLD  8774  inf3lem2  9125  infpssr  9768  ssfin4  9770  genpnnp  10465  ltexprlem1  10496  reclem2pr  10508  mrieqv2d  16968  lbspss  19922  lsmcv  19981  lidlnz  20069  obslbs  20495  nmoid  23444  spansncvi  29534  fvineqsneq  35109  lsat0cv  36609  osumcllem11N  37542  pexmidlem8N  37553  isomenndlem  43535
 Copyright terms: Public domain W3C validator