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

Theorem sseq0 4171
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 3823 . . 3 (𝐵 = ∅ → (𝐴𝐵𝐴 ⊆ ∅))
2 ss0 4170 . . 3 (𝐴 ⊆ ∅ → 𝐴 = ∅)
31, 2syl6bi 245 . 2 (𝐵 = ∅ → (𝐴𝐵𝐴 = ∅))
43impcom 397 1 ((𝐴𝐵𝐵 = ∅) → 𝐴 = ∅)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 385   = wceq 1653  wss 3769  c0 4115
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-ext 2777
This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-clab 2786  df-cleq 2792  df-clel 2795  df-nfc 2930  df-v 3387  df-dif 3772  df-in 3776  df-ss 3783  df-nul 4116
This theorem is referenced by:  ssn0  4172  ssdifin0  4244  disjxiun  4840  undom  8290  fieq0  8569  infdifsn  8804  cantnff  8821  tc00  8874  hashun3  13423  strleun  16293  xpsc0  16535  xpsc1  16536  dmdprdsplit2lem  18760  2idlval  19556  opsrle  19798  pf1rcl  20035  ocvval  20336  pjfval  20375  en2top  21118  nrmsep  21490  isnrm3  21492  regsep2  21509  xkohaus  21785  kqdisj  21864  regr1lem  21871  alexsublem  22176  reconnlem1  22957  metdstri  22982  iundisj2  23657  0clwlk0  27476  disjxpin  29918  iundisj2f  29920  iundisj2fi  30074  cvmsss2  31773  cldbnd  32833  cntotbnd  34082  mapfzcons1  38066  onfrALTlem2  39532  onfrALTlem2VD  39885  nnuzdisj  40315
  Copyright terms: Public domain W3C validator