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 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 = ∅) → 𝐴 = ∅)

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1568   ⊆ wss 3904  ∅c0 4285

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1571  df-fal 1581  df-ex 1808  df-sb 2095  df-clab 2740  df-cleq 2753  df-clel 2836  df-dif 3907  df-ss 3921  df-nul 4286

This theorem is referenced by:  ssn0  4361  ssdifin0  4445  disjxiun  5105  f1un  6841  fsetexb  8860  infn0  9261  fieq0  9380  infdifsn  9625  cantnff  9642  tc00  9714  hashun3  14420  strleun  17216  dmdprdsplit2lem  20116  2idlval  21369  ocvval  21796  pjfval  21835  opsrle  22177  pf1rcl  22488  en2top  23121  nrmsep  23493  isnrm3  23495  regsep2  23512  xkohaus  23789  kqdisj  23868  regr1lem  23875  alexsublem  24180  reconnlem1  24963  metdstri  24988  iundisj2  25687  left0s  28062  right0s  28063  0clwlk0  30449  disjxpin  32899  iundisj2f  32901  iundisj2fi  33108  1arithufdlem4  33803  cvmsss2  35732  cldbnd  36803  cntotbnd  38413  nna4b4nsq  43362  mapfzcons1  43418  onfrALTlem2  45225  onfrALTlem2VD  45567  nnuzdisj  46041  ssdisjd  49553  ssdisjdr  49554  sepnsepolem2  49668  sepnsepo  49669  resccat  49819