Theorem sseq0 4364

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 3973	. . 3 ⊢ (𝐵 = ∅ → (𝐴 ⊆ 𝐵 ↔ 𝐴 ⊆ ∅))
2		ss0 4363	. . 3 ⊢ (𝐴 ⊆ ∅ → 𝐴 = ∅)
3	1, 2	syl6bi 252	. 2 ⊢ (𝐵 = ∅ → (𝐴 ⊆ 𝐵 → 𝐴 = ∅))
4	3	impcom 408	1 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 = ∅) → 𝐴 = ∅)

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1541   ⊆ wss 3913  ∅c0 4287

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-v 3448  df-dif 3916  df-in 3920  df-ss 3930  df-nul 4288

This theorem is referenced by:  ssn0  4365  ssdifin0  4448  disjxiun  5107  f1un  6809  fsetexb  8809  undomOLD  9011  infn0  9258  fieq0  9366  infdifsn  9602  cantnff  9619  tc00  9693  hashun3  14294  strleun  17040  dmdprdsplit2lem  19838  2idlval  20762  ocvval  21108  pjfval  21149  opsrle  21485  pf1rcl  21752  en2top  22372  nrmsep  22745  isnrm3  22747  regsep2  22764  xkohaus  23041  kqdisj  23120  regr1lem  23127  alexsublem  23432  reconnlem1  24226  metdstri  24251  iundisj2  24950  left0s  27265  right0s  27266  0clwlk0  29139  disjxpin  31573  iundisj2f  31575  iundisj2fi  31768  cvmsss2  33955  cldbnd  34874  cntotbnd  36328  nna4b4nsq  41056  mapfzcons1  41098  onfrALTlem2  42950  onfrALTlem2VD  43293  nnuzdisj  43710  ssdisjd  47012  ssdisjdr  47013  sepnsepolem2  47075  sepnsepo  47076