Theorem sseq0 4333

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		sseq2 3947	. . 3 ⊢ (𝐵 = ∅ → (𝐴 ⊆ 𝐵 ↔ 𝐴 ⊆ ∅))
2		ss0 4332	. . 3 ⊢ (𝐴 ⊆ ∅ → 𝐴 = ∅)
3	1, 2	syl6bi 252	. 2 ⊢ (𝐵 = ∅ → (𝐴 ⊆ 𝐵 → 𝐴 = ∅))
4	3	impcom 408	1 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 = ∅) → 𝐴 = ∅)

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1539   ⊆ wss 3887  ∅c0 4256

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3434  df-dif 3890  df-in 3894  df-ss 3904  df-nul 4257

This theorem is referenced by:  ssn0  4334  ssdifin0  4416  disjxiun  5071  f1un  6736  fsetexb  8652  undomOLD  8847  fieq0  9180  infdifsn  9415  cantnff  9432  tc00  9506  hashun3  14099  strleun  16858  dmdprdsplit2lem  19648  2idlval  20504  ocvval  20872  pjfval  20913  opsrle  21248  pf1rcl  21515  en2top  22135  nrmsep  22508  isnrm3  22510  regsep2  22527  xkohaus  22804  kqdisj  22883  regr1lem  22890  alexsublem  23195  reconnlem1  23989  metdstri  24014  iundisj2  24713  0clwlk0  28496  disjxpin  30927  iundisj2f  30929  iundisj2fi  31118  cvmsss2  33236  left0s  34075  right0s  34076  cldbnd  34515  cntotbnd  35954  nna4b4nsq  40497  mapfzcons1  40539  onfrALTlem2  42166  onfrALTlem2VD  42509  nnuzdisj  42894  ssdisjd  46153  ssdisjdr  46154  sepnsepolem2  46216  sepnsepo  46217