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

Theorem pssdifn0 4358
Description: A proper subclass has a nonempty difference. (Contributed by NM, 3-May-1994.)
Assertion
Ref Expression
pssdifn0 ((𝐴𝐵𝐴𝐵) → (𝐵𝐴) ≠ ∅)

Proof of Theorem pssdifn0
StepHypRef Expression
1 ssdif0 4356 . . . 4 (𝐵𝐴 ↔ (𝐵𝐴) = ∅)
2 eqss 3990 . . . . 5 (𝐴 = 𝐵 ↔ (𝐴𝐵𝐵𝐴))
32simplbi2 500 . . . 4 (𝐴𝐵 → (𝐵𝐴𝐴 = 𝐵))
41, 3biimtrrid 242 . . 3 (𝐴𝐵 → ((𝐵𝐴) = ∅ → 𝐴 = 𝐵))
54necon3d 2953 . 2 (𝐴𝐵 → (𝐴𝐵 → (𝐵𝐴) ≠ ∅))
65imp 406 1 ((𝐴𝐵𝐴𝐵) → (𝐵𝐴) ≠ ∅)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395   = wceq 1533  wne 2932  cdif 3938  wss 3941  c0 4315
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 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2695
This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2702  df-cleq 2716  df-clel 2802  df-ne 2933  df-v 3468  df-dif 3944  df-in 3948  df-ss 3958  df-nul 4316
This theorem is referenced by:  pssdif  4359  tz7.7  6381  domdifsn  9051  inf3lem3  9622  isf32lem6  10350  fclscf  23853  flimfnfcls  23856  lebnumlem1  24811  lebnumlem2  24812  lebnumlem3  24813  ig1peu  26031  ig1pdvds  26036  qsidomlem2  33044  qsdrng  33083  divrngidl  37390
  Copyright terms: Public domain W3C validator