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

Theorem sseq0 4360
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 3971 . . 3 (𝐵 = ∅ → (𝐴𝐵𝐴 ⊆ ∅))
2 ss0 4359 . . 3 (𝐴 ⊆ ∅ → 𝐴 = ∅)
31, 2syl6bi 253 . 2 (𝐵 = ∅ → (𝐴𝐵𝐴 = ∅))
43impcom 409 1 ((𝐴𝐵𝐵 = ∅) → 𝐴 = ∅)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397   = wceq 1542  wss 3911  c0 4283
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-v 3448  df-dif 3914  df-in 3918  df-ss 3928  df-nul 4284
This theorem is referenced by:  ssn0  4361  ssdifin0  4444  disjxiun  5103  f1un  6805  fsetexb  8803  undomOLD  9005  infn0  9252  fieq0  9358  infdifsn  9594  cantnff  9611  tc00  9685  hashun3  14285  strleun  17030  dmdprdsplit2lem  19825  2idlval  20706  ocvval  21074  pjfval  21115  opsrle  21451  pf1rcl  21718  en2top  22338  nrmsep  22711  isnrm3  22713  regsep2  22730  xkohaus  23007  kqdisj  23086  regr1lem  23093  alexsublem  23398  reconnlem1  24192  metdstri  24217  iundisj2  24916  left0s  27225  right0s  27226  0clwlk0  29079  disjxpin  31509  iundisj2f  31511  iundisj2fi  31703  cvmsss2  33871  cldbnd  34801  cntotbnd  36258  nna4b4nsq  41001  mapfzcons1  41043  onfrALTlem2  42835  onfrALTlem2VD  43178  nnuzdisj  43596  ssdisjd  46899  ssdisjdr  46900  sepnsepolem2  46962  sepnsepo  46963
  Copyright terms: Public domain W3C validator