Theorem sseq0 4117

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

Syntax hints:   → wi 4   ∧ wa 382   = wceq 1630   ⊆ wss 3721  ∅c0 4061

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1990  ax-6 2056  ax-7 2092  ax-9 2153  ax-10 2173  ax-11 2189  ax-12 2202  ax-13 2407  ax-ext 2750

This theorem depends on definitions:  df-bi 197  df-an 383  df-or 827  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2049  df-clab 2757  df-cleq 2763  df-clel 2766  df-nfc 2901  df-v 3351  df-dif 3724  df-in 3728  df-ss 3735  df-nul 4062

This theorem is referenced by:  ssn0  4118  ssdifin0  4190  disjxiun  4781  undom  8203  fieq0  8482  infdifsn  8717  cantnff  8734  tc00  8787  hashun3  13374  strlemor1OLD  16176  strleun  16179  xpsc0  16427  xpsc1  16428  dmdprdsplit2lem  18651  2idlval  19447  opsrle  19689  pf1rcl  19927  ocvval  20227  pjfval  20266  en2top  21009  nrmsep  21381  isnrm3  21383  regsep2  21400  xkohaus  21676  kqdisj  21755  regr1lem  21762  alexsublem  22067  reconnlem1  22848  metdstri  22873  iundisj2  23536  0clwlk0  27309  disjxpin  29733  iundisj2f  29735  iundisj2fi  29890  cvmsss2  31588  cldbnd  32652  cntotbnd  33920  mapfzcons1  37799  onfrALTlem2  39280  onfrALTlem2VD  39641  nnuzdisj  40081