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

Theorem sseq0 4120
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 3776 . . 3 (𝐵 = ∅ → (𝐴𝐵𝐴 ⊆ ∅))
2 ss0 4119 . . 3 (𝐴 ⊆ ∅ → 𝐴 = ∅)
31, 2syl6bi 243 . 2 (𝐵 = ∅ → (𝐴𝐵𝐴 = ∅))
43impcom 394 1 ((𝐴𝐵𝐵 = ∅) → 𝐴 = ∅)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382   = wceq 1631  wss 3723  c0 4063
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-v 3353  df-dif 3726  df-in 3730  df-ss 3737  df-nul 4064
This theorem is referenced by:  ssn0  4121  ssdifin0  4193  disjxiun  4784  undom  8208  fieq0  8487  infdifsn  8722  cantnff  8739  tc00  8792  hashun3  13375  strlemor1OLD  16177  strleun  16180  xpsc0  16428  xpsc1  16429  dmdprdsplit2lem  18652  2idlval  19448  opsrle  19690  pf1rcl  19928  ocvval  20228  pjfval  20267  en2top  21010  nrmsep  21382  isnrm3  21384  regsep2  21401  xkohaus  21677  kqdisj  21756  regr1lem  21763  alexsublem  22068  reconnlem1  22849  metdstri  22874  iundisj2  23537  0clwlk0  27312  disjxpin  29739  iundisj2f  29741  iundisj2fi  29896  cvmsss2  31594  cldbnd  32658  cntotbnd  33925  mapfzcons1  37804  onfrALTlem2  39284  onfrALTlem2VD  39645  nnuzdisj  40082
  Copyright terms: Public domain W3C validator