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

Theorem pssnel 4423
 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 4330 . . 3 (𝐴𝐵 → (𝐵𝐴) ≠ ∅)
2 n0 4314 . . 3 ((𝐵𝐴) ≠ ∅ ↔ ∃𝑥 𝑥 ∈ (𝐵𝐴))
31, 2sylib 219 . 2 (𝐴𝐵 → ∃𝑥 𝑥 ∈ (𝐵𝐴))
4 eldif 3950 . . 3 (𝑥 ∈ (𝐵𝐴) ↔ (𝑥𝐵 ∧ ¬ 𝑥𝐴))
54exbii 1841 . 2 (∃𝑥 𝑥 ∈ (𝐵𝐴) ↔ ∃𝑥(𝑥𝐵 ∧ ¬ 𝑥𝐴))
63, 5sylib 219 1 (𝐴𝐵 → ∃𝑥(𝑥𝐵 ∧ ¬ 𝑥𝐴))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 396  ∃wex 1773   ∈ wcel 2107   ≠ wne 3021   ∖ cdif 3937   ⊊ wpss 3941  ∅c0 4295 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2798 This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2805  df-cleq 2819  df-clel 2898  df-nfc 2968  df-ne 3022  df-v 3502  df-dif 3943  df-in 3947  df-ss 3956  df-pss 3958  df-nul 4296 This theorem is referenced by:  php  8695  php3  8697  pssnn  8730  inf3lem2  9086  infpssr  9724  ssfin4  9726  genpnnp  10421  ltexprlem1  10452  reclem2pr  10464  mrieqv2d  16905  lbspss  19790  lsmcv  19849  lidlnz  19936  obslbs  20809  nmoid  23285  spansncvi  29362  fvineqsneq  34581  lsat0cv  36055  osumcllem11N  36988  pexmidlem8N  36999  isomenndlem  42697
 Copyright terms: Public domain W3C validator