Theorem sseq0 4360

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 3965	. . 3 ⊢ (𝐵 = ∅ → (𝐴 ⊆ 𝐵 ↔ 𝐴 ⊆ ∅))
2		ss0 4359	. . 3 ⊢ (𝐴 ⊆ ∅ → 𝐴 = ∅)
3	1, 2	biimtrdi 256	. 2 ⊢ (𝐵 = ∅ → (𝐴 ⊆ 𝐵 → 𝐴 = ∅))
4	3	impcom 412	1 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 = ∅) → 𝐴 = ∅)

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1563   ⊆ wss 3907  ∅c0 4288

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1566  df-fal 1576  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-dif 3910  df-ss 3924  df-nul 4289

This theorem is referenced by:  ssn0  4361  ssdifin0  4442  disjxiun  5102  f1un  6831  fsetexb  8849  infn0  9250  fieq0  9369  infdifsn  9614  cantnff  9631  tc00  9703  hashun3  14411  strleun  17207  dmdprdsplit2lem  20108  2idlval  21352  ocvval  21777  pjfval  21816  opsrle  22158  pf1rcl  22470  en2top  23103  nrmsep  23475  isnrm3  23477  regsep2  23494  xkohaus  23771  kqdisj  23850  regr1lem  23857  alexsublem  24162  reconnlem1  24945  metdstri  24970  iundisj2  25669  left0s  28044  right0s  28045  0clwlk0  30392  disjxpin  32843  iundisj2f  32845  iundisj2fi  33054  1arithufdlem4  33754  cvmsss2  35637  cldbnd  36699  cntotbnd  38307  nna4b4nsq  43254  mapfzcons1  43310  onfrALTlem2  45120  onfrALTlem2VD  45462  nnuzdisj  45929  ssdisjd  49437  ssdisjdr  49438  sepnsepolem2  49552  sepnsepo  49553  resccat  49703