Theorem sseq0 4120

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 3776	. . 3 ⊢ (𝐵 = ∅ → (𝐴 ⊆ 𝐵 ↔ 𝐴 ⊆ ∅))
2		ss0 4119	. . 3 ⊢ (𝐴 ⊆ ∅ → 𝐴 = ∅)
3	1, 2	syl6bi 243	. 2 ⊢ (𝐵 = ∅ → (𝐴 ⊆ 𝐵 → 𝐴 = ∅))
4	3	impcom 394	1 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 = ∅) → 𝐴 = ∅)

Syntax hints:   → wi 4   ∧ wa 382   = wceq 1631   ⊆ wss 3723  ∅c0 4063

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751

This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-v 3353  df-dif 3726  df-in 3730  df-ss 3737  df-nul 4064

This theorem is referenced by:  ssn0  4121  ssdifin0  4193  disjxiun  4784  undom  8208  fieq0  8487  infdifsn  8722  cantnff  8739  tc00  8792  hashun3  13375  strlemor1OLD  16177  strleun  16180  xpsc0  16428  xpsc1  16429  dmdprdsplit2lem  18652  2idlval  19448  opsrle  19690  pf1rcl  19928  ocvval  20228  pjfval  20267  en2top  21010  nrmsep  21382  isnrm3  21384  regsep2  21401  xkohaus  21677  kqdisj  21756  regr1lem  21763  alexsublem  22068  reconnlem1  22849  metdstri  22874  iundisj2  23537  0clwlk0  27312  disjxpin  29739  iundisj2f  29741  iundisj2fi  29896  cvmsss2  31594  cldbnd  32658  cntotbnd  33925  mapfzcons1  37804  onfrALTlem2  39284  onfrALTlem2VD  39645  nnuzdisj  40082