Theorem sseq0 3927

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 3590	. . 3 ⊢ (𝐵 = ∅ → (𝐴 ⊆ 𝐵 ↔ 𝐴 ⊆ ∅))
2		ss0 3926	. . 3 ⊢ (𝐴 ⊆ ∅ → 𝐴 = ∅)
3	1, 2	syl6bi 242	. 2 ⊢ (𝐵 = ∅ → (𝐴 ⊆ 𝐵 → 𝐴 = ∅))
4	3	impcom 445	1 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 = ∅) → 𝐴 = ∅)

Syntax hints:   → wi 4   ∧ wa 383   = wceq 1475   ⊆ wss 3540  ∅c0 3874

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-dif 3543  df-in 3547  df-ss 3554  df-nul 3875

This theorem is referenced by:  ssn0  3928  ssdifin0  4002  disjxiun  4579  disjxiunOLD  4580  undom  7933  fieq0  8210  infdifsn  8437  cantnff  8454  tc00  8507  hashun3  13034  strlemor1  15796  strleun  15799  xpsc0  16043  xpsc1  16044  dmdprdsplit2lem  18267  2idlval  19054  opsrle  19296  pf1rcl  19534  ocvval  19830  pjfval  19869  en2top  20600  nrmsep  20971  isnrm3  20973  regsep2  20990  xkohaus  21266  kqdisj  21345  regr1lem  21352  alexsublem  21658  reconnlem1  22437  metdstri  22462  iundisj2  23124  clwlk0  26290  disjxpin  28783  iundisj2f  28785  iundisj2fi  28943  cvmsss2  30510  cldbnd  31491  cntotbnd  32765  mapfzcons1  36298  onfrALTlem2  37782  onfrALTlem2VD  38147  nnuzdisj  38512  0clwlk0  41299