Theorem sseq0 4356

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 3961	. . 3 ⊢ (𝐵 = ∅ → (𝐴 ⊆ 𝐵 ↔ 𝐴 ⊆ ∅))
2		ss0 4355	. . 3 ⊢ (𝐴 ⊆ ∅ → 𝐴 = ∅)
3	1, 2	biimtrdi 253	. 2 ⊢ (𝐵 = ∅ → (𝐴 ⊆ 𝐵 → 𝐴 = ∅))
4	3	impcom 407	1 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 = ∅) → 𝐴 = ∅)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542   ⊆ wss 3902  ∅c0 4286

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-dif 3905  df-ss 3919  df-nul 4287

This theorem is referenced by:  ssn0  4357  ssdifin0  4439  disjxiun  5096  f1un  6795  fsetexb  8805  infn0  9206  fieq0  9328  infdifsn  9570  cantnff  9587  tc00  9659  hashun3  14311  strleun  17088  dmdprdsplit2lem  19980  2idlval  21210  ocvval  21626  pjfval  21665  opsrle  22006  pf1rcl  22297  en2top  22933  nrmsep  23305  isnrm3  23307  regsep2  23324  xkohaus  23601  kqdisj  23680  regr1lem  23687  alexsublem  23992  reconnlem1  24775  metdstri  24800  iundisj2  25510  left0s  27875  right0s  27876  0clwlk0  30190  disjxpin  32645  iundisj2f  32647  iundisj2fi  32858  1arithufdlem4  33609  cvmsss2  35449  cldbnd  36501  cntotbnd  37968  nna4b4nsq  42939  mapfzcons1  42995  onfrALTlem2  44823  onfrALTlem2VD  45165  nnuzdisj  45636  ssdisjd  49089  ssdisjdr  49090  sepnsepolem2  49204  sepnsepo  49205  resccat  49355