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

Theorem pssnel 3991
 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 3899 . . 3 (𝐴𝐵 → (𝐵𝐴) ≠ ∅)
2 n0 3890 . . 3 ((𝐵𝐴) ≠ ∅ ↔ ∃𝑥 𝑥 ∈ (𝐵𝐴))
31, 2sylib 207 . 2 (𝐴𝐵 → ∃𝑥 𝑥 ∈ (𝐵𝐴))
4 eldif 3550 . . 3 (𝑥 ∈ (𝐵𝐴) ↔ (𝑥𝐵 ∧ ¬ 𝑥𝐴))
54exbii 1764 . 2 (∃𝑥 𝑥 ∈ (𝐵𝐴) ↔ ∃𝑥(𝑥𝐵 ∧ ¬ 𝑥𝐴))
63, 5sylib 207 1 (𝐴𝐵 → ∃𝑥(𝑥𝐵 ∧ ¬ 𝑥𝐴))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 383  ∃wex 1695   ∈ wcel 1977   ≠ wne 2780   ∖ cdif 3537   ⊊ wpss 3541  ∅c0 3874 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-v 3175  df-dif 3543  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875 This theorem is referenced by:  php  8029  php3  8031  pssnn  8063  inf3lem2  8409  infpssr  9013  ssfin4  9015  genpnnp  9706  ltexprlem1  9737  reclem2pr  9749  mrieqv2d  16122  lbspss  18903  lsmcv  18962  lidlnz  19049  obslbs  19893  nmoid  22356  spansncvi  27895  lsat0cv  33338  osumcllem11N  34270  pexmidlem8N  34281  isomenndlem  39420
 Copyright terms: Public domain W3C validator