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

Theorem sseq0 3947
 Description: A subclass of an empty class is empty. (Contributed by NM, 7-Mar-2007.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
Assertion
Ref Expression
sseq0 ((𝐴𝐵𝐵 = ∅) → 𝐴 = ∅)

Proof of Theorem sseq0
StepHypRef Expression
1 sseq2 3606 . . 3 (𝐵 = ∅ → (𝐴𝐵𝐴 ⊆ ∅))
2 ss0 3946 . . 3 (𝐴 ⊆ ∅ → 𝐴 = ∅)
31, 2syl6bi 243 . 2 (𝐵 = ∅ → (𝐴𝐵𝐴 = ∅))
43impcom 446 1 ((𝐴𝐵𝐵 = ∅) → 𝐴 = ∅)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 384   = wceq 1480   ⊆ wss 3555  ∅c0 3891 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601 This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-v 3188  df-dif 3558  df-in 3562  df-ss 3569  df-nul 3892 This theorem is referenced by:  ssn0  3948  ssdifin0  4022  disjxiun  4609  disjxiunOLD  4610  undom  7992  fieq0  8271  infdifsn  8498  cantnff  8515  tc00  8568  hashun3  13113  strlemor1OLD  15890  strleun  15893  xpsc0  16141  xpsc1  16142  dmdprdsplit2lem  18365  2idlval  19152  opsrle  19394  pf1rcl  19632  ocvval  19930  pjfval  19969  en2top  20700  nrmsep  21071  isnrm3  21073  regsep2  21090  xkohaus  21366  kqdisj  21445  regr1lem  21452  alexsublem  21758  reconnlem1  22537  metdstri  22562  iundisj2  23224  0clwlk0  26858  disjxpin  29246  iundisj2f  29248  iundisj2fi  29397  cvmsss2  30964  cldbnd  31963  cntotbnd  33227  mapfzcons1  36760  onfrALTlem2  38243  onfrALTlem2VD  38608  nnuzdisj  39035
 Copyright terms: Public domain W3C validator