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

Theorem sseq0 4336
 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 3979 . . 3 (𝐵 = ∅ → (𝐴𝐵𝐴 ⊆ ∅))
2 ss0 4335 . . 3 (𝐴 ⊆ ∅ → 𝐴 = ∅)
31, 2syl6bi 256 . 2 (𝐵 = ∅ → (𝐴𝐵𝐴 = ∅))
43impcom 411 1 ((𝐴𝐵𝐵 = ∅) → 𝐴 = ∅)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399   = wceq 1538   ⊆ wss 3919  ∅c0 4276 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-ext 2796 This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2071  df-clab 2803  df-cleq 2817  df-clel 2896  df-v 3482  df-dif 3922  df-in 3926  df-ss 3936  df-nul 4277 This theorem is referenced by:  ssn0  4337  ssdifin0  4414  disjxiun  5049  undom  8601  fieq0  8882  infdifsn  9117  cantnff  9134  tc00  9187  hashun3  13750  strleun  16591  dmdprdsplit2lem  19167  2idlval  20006  ocvval  20413  pjfval  20452  opsrle  20722  pf1rcl  20980  en2top  21596  nrmsep  21968  isnrm3  21970  regsep2  21987  xkohaus  22264  kqdisj  22343  regr1lem  22350  alexsublem  22655  reconnlem1  23437  metdstri  23462  iundisj2  24159  0clwlk0  27923  disjxpin  30352  iundisj2f  30354  iundisj2fi  30534  cvmsss2  32581  cldbnd  33734  cntotbnd  35182  mapfzcons1  39578  onfrALTlem2  41176  onfrALTlem2VD  41519  nnuzdisj  41917
 Copyright terms: Public domain W3C validator