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

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 400   = wceq 1569   ⊆ wss 3904  ∅c0 4285

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 401  df-tru 1572  df-fal 1582  df-ex 1809  df-sb 2096  df-clab 2741  df-cleq 2754  df-clel 2837  df-dif 3907  df-ss 3921  df-nul 4286

This theorem is used by:  ssn0  4361  ssdifin0  4445  disjxiun  5105  f1un  6841  fsetexb  8859  infn0  9260  fieq0  9379  infdifsn  9624  cantnff  9641  tc00  9713  hashun3  14427  strleun  17223  dmdprdsplit2lem  20123  2idlval  21401  ocvval  21828  pjfval  21867  opsrle  22209  pf1rcl  22520  en2top  23153  nrmsep  23525  isnrm3  23527  regsep2  23544  xkohaus  23821  kqdisj  23900  regr1lem  23907  alexsublem  24212  reconnlem1  24995  metdstri  25020  iundisj2  25719  left0s  28097  right0s  28098  0clwlk0  30494  disjxpin  32944  iundisj2f  32946  iundisj2fi  33153  1arithufdlem4  33846  cvmsss2  35774  cldbnd  36865  cntotbnd  38475  nna4b4nsq  43420  mapfzcons1  43476  onfrALTlem2  45283  onfrALTlem2VD  45625  nnuzdisj  46099  ssdisjd  49614  ssdisjdr  49615  sepnsepolem2  49729  sepnsepo  49730  resccat  49880