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

Theorem pssdifn0 4360
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 4358 . . . 4 (𝐵𝐴 ↔ (𝐵𝐴) = ∅)
2 eqss 3992 . . . . 5 (𝐴 = 𝐵 ↔ (𝐴𝐵𝐵𝐴))
32simplbi2 500 . . . 4 (𝐴𝐵 → (𝐵𝐴𝐴 = 𝐵))
41, 3biimtrrid 242 . . 3 (𝐴𝐵 → ((𝐵𝐴) = ∅ → 𝐴 = 𝐵))
54necon3d 2955 . 2 (𝐴𝐵 → (𝐴𝐵 → (𝐵𝐴) ≠ ∅))
65imp 406 1 ((𝐴𝐵𝐴𝐵) → (𝐵𝐴) ≠ ∅)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395   = wceq 1533  wne 2934  cdif 3940  wss 3943  c0 4317
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 2697
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 2704  df-cleq 2718  df-clel 2804  df-ne 2935  df-v 3470  df-dif 3946  df-in 3950  df-ss 3960  df-nul 4318
This theorem is referenced by:  pssdif  4361  tz7.7  6384  domdifsn  9056  inf3lem3  9627  isf32lem6  10355  fclscf  23884  flimfnfcls  23887  lebnumlem1  24842  lebnumlem2  24843  lebnumlem3  24844  ig1peu  26064  ig1pdvds  26069  qsidomlem2  33078  qsdrng  33117  divrngidl  37409
  Copyright terms: Public domain W3C validator