Theorem sseq0 4353

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

Step	Hyp	Ref	Expression
1		sseq0b 4352	. 2 ⊢ (𝐵 = ∅ → (𝐴 ⊆ 𝐵 ↔ 𝐴 = ∅))
2	1	biimpac 484	1 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 = ∅) → 𝐴 = ∅)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1569   ⊆ wss 3895  ∅c0 4278

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ss 3896  df-dif 4047  df-nul 4279

This theorem is used by:  ssn0  4354  ssdifin0  4440  disjxiun  5099  f1un  6845  fsetexb  8887  infn0  9295  fieq0  9414  infdifsn  9659  cantnff  9676  tc00  9748  hashun3  14529  strleun  17336  dmdprdsplit2lem  20262  2idlval  21545  ocvval  21974  pjfval  22013  opsrle  22357  pf1rcl  22668  en2top  23304  nrmsep  23676  isnrm3  23678  regsep2  23695  xkohaus  23973  kqdisj  24052  regr1lem  24059  alexsublem  24364  reconnlem1  25147  metdstri  25172  iundisj2  25871  left0s  28280  right0s  28281  0clwlk0  30724  disjxpin  33225  iundisj2f  33227  iundisj2fi  33432  1arithufdlem4  34122  cvmsss2  36108  cldbnd  37189  cntotbnd  38806  mapfzcons1  43804  onfrALTlem2  45605  onfrALTlem2VD  45947  nnuzdisj  46443  ssdisjd  49994  ssdisjdr  49995  sepnsepolem2  50107  sepnsepo  50108  resccat  50258