Theorem sseq0 4357

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542   ⊆ wss 3903  ∅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 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 3906  df-ss 3920  df-nul 4288

This theorem is referenced by:  ssn0  4358  ssdifin0  4440  disjxiun  5097  f1un  6802  fsetexb  8813  infn0  9214  fieq0  9336  infdifsn  9578  cantnff  9595  tc00  9667  hashun3  14319  strleun  17096  dmdprdsplit2lem  19988  2idlval  21218  ocvval  21634  pjfval  21673  opsrle  22014  pf1rcl  22305  en2top  22941  nrmsep  23313  isnrm3  23315  regsep2  23332  xkohaus  23609  kqdisj  23688  regr1lem  23695  alexsublem  24000  reconnlem1  24783  metdstri  24808  iundisj2  25518  left0s  27901  right0s  27902  0clwlk0  30219  disjxpin  32674  iundisj2f  32676  iundisj2fi  32887  1arithufdlem4  33639  cvmsss2  35487  cldbnd  36539  cntotbnd  38036  nna4b4nsq  43007  mapfzcons1  43063  onfrALTlem2  44891  onfrALTlem2VD  45233  nnuzdisj  45703  ssdisjd  49156  ssdisjdr  49157  sepnsepolem2  49271  sepnsepo  49272  resccat  49422