Theorem sseq0 4307

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 3941	. . 3 ⊢ (𝐵 = ∅ → (𝐴 ⊆ 𝐵 ↔ 𝐴 ⊆ ∅))
2		ss0 4306	. . 3 ⊢ (𝐴 ⊆ ∅ → 𝐴 = ∅)
3	1, 2	syl6bi 256	. 2 ⊢ (𝐵 = ∅ → (𝐴 ⊆ 𝐵 → 𝐴 = ∅))
4	3	impcom 411	1 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 = ∅) → 𝐴 = ∅)

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1538   ⊆ wss 3881  ∅c0 4243

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-dif 3884  df-in 3888  df-ss 3898  df-nul 4244

This theorem is referenced by:  ssn0  4308  ssdifin0  4389  disjxiun  5027  undom  8588  fieq0  8869  infdifsn  9104  cantnff  9121  tc00  9174  hashun3  13741  strleun  16583  dmdprdsplit2lem  19160  2idlval  19999  ocvval  20356  pjfval  20395  opsrle  20715  pf1rcl  20973  en2top  21590  nrmsep  21962  isnrm3  21964  regsep2  21981  xkohaus  22258  kqdisj  22337  regr1lem  22344  alexsublem  22649  reconnlem1  23431  metdstri  23456  iundisj2  24153  0clwlk0  27917  disjxpin  30351  iundisj2f  30353  iundisj2fi  30546  cvmsss2  32634  cldbnd  33787  cntotbnd  35234  mapfzcons1  39658  onfrALTlem2  41252  onfrALTlem2VD  41595  nnuzdisj  41987