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 1570   ⊆ wss 3898  ∅c0 4278

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-dif 3901  df-ss 3915  df-nul 4279

This theorem is used by:  ssn0  4354  ssdifin0  4440  disjxiun  5099  f1un  6833  fsetexb  8864  infn0  9272  fieq0  9391  infdifsn  9636  cantnff  9653  tc00  9725  hashun3  14496  strleun  17297  dmdprdsplit2lem  20223  2idlval  21506  ocvval  21935  pjfval  21974  opsrle  22318  pf1rcl  22629  en2top  23265  nrmsep  23637  isnrm3  23639  regsep2  23656  xkohaus  23934  kqdisj  24013  regr1lem  24020  alexsublem  24325  reconnlem1  25108  metdstri  25133  iundisj2  25832  left0s  28213  right0s  28214  0clwlk0  30657  disjxpin  33116  iundisj2f  33118  iundisj2fi  33323  1arithufdlem4  34013  cvmsss2  35960  cldbnd  37036  cntotbnd  38650  nna4b4nsq  43610  mapfzcons1  43666  onfrALTlem2  45473  onfrALTlem2VD  45815  nnuzdisj  46289  ssdisjd  49840  ssdisjdr  49841  sepnsepolem2  49953  sepnsepo  49954  resccat  50104