Theorem sseq0 4355

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 3995	. . 3 ⊢ (𝐵 = ∅ → (𝐴 ⊆ 𝐵 ↔ 𝐴 ⊆ ∅))
2		ss0 4354	. . 3 ⊢ (𝐴 ⊆ ∅ → 𝐴 = ∅)
3	1, 2	syl6bi 255	. 2 ⊢ (𝐵 = ∅ → (𝐴 ⊆ 𝐵 → 𝐴 = ∅))
4	3	impcom 410	1 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 = ∅) → 𝐴 = ∅)

Syntax hints:   → wi 4   ∧ wa 398   = wceq 1537   ⊆ wss 3938  ∅c0 4293

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-dif 3941  df-in 3945  df-ss 3954  df-nul 4294

This theorem is referenced by:  ssn0  4356  ssdifin0  4433  disjxiun  5065  undom  8607  fieq0  8887  infdifsn  9122  cantnff  9139  tc00  9192  hashun3  13748  strleun  16593  dmdprdsplit2lem  19169  2idlval  20008  opsrle  20258  pf1rcl  20514  ocvval  20813  pjfval  20852  en2top  21595  nrmsep  21967  isnrm3  21969  regsep2  21986  xkohaus  22263  kqdisj  22342  regr1lem  22349  alexsublem  22654  reconnlem1  23436  metdstri  23461  iundisj2  24152  0clwlk0  27913  disjxpin  30340  iundisj2f  30342  iundisj2fi  30522  cvmsss2  32523  cldbnd  33676  cntotbnd  35076  mapfzcons1  39321  onfrALTlem2  40887  onfrALTlem2VD  41230  nnuzdisj  41630