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

Theorem sseq0 4117
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 3774 . . 3 (𝐵 = ∅ → (𝐴𝐵𝐴 ⊆ ∅))
2 ss0 4116 . . 3 (𝐴 ⊆ ∅ → 𝐴 = ∅)
31, 2syl6bi 243 . 2 (𝐵 = ∅ → (𝐴𝐵𝐴 = ∅))
43impcom 394 1 ((𝐴𝐵𝐵 = ∅) → 𝐴 = ∅)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382   = wceq 1630  wss 3721  c0 4061
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1990  ax-6 2056  ax-7 2092  ax-9 2153  ax-10 2173  ax-11 2189  ax-12 2202  ax-13 2407  ax-ext 2750
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 827  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2049  df-clab 2757  df-cleq 2763  df-clel 2766  df-nfc 2901  df-v 3351  df-dif 3724  df-in 3728  df-ss 3735  df-nul 4062
This theorem is referenced by:  ssn0  4118  ssdifin0  4190  disjxiun  4781  undom  8203  fieq0  8482  infdifsn  8717  cantnff  8734  tc00  8787  hashun3  13374  strlemor1OLD  16176  strleun  16179  xpsc0  16427  xpsc1  16428  dmdprdsplit2lem  18651  2idlval  19447  opsrle  19689  pf1rcl  19927  ocvval  20227  pjfval  20266  en2top  21009  nrmsep  21381  isnrm3  21383  regsep2  21400  xkohaus  21676  kqdisj  21755  regr1lem  21762  alexsublem  22067  reconnlem1  22848  metdstri  22873  iundisj2  23536  0clwlk0  27309  disjxpin  29733  iundisj2f  29735  iundisj2fi  29890  cvmsss2  31588  cldbnd  32652  cntotbnd  33920  mapfzcons1  37799  onfrALTlem2  39280  onfrALTlem2VD  39641  nnuzdisj  40081
  Copyright terms: Public domain W3C validator