Theorem sseq0 4344

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

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

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 3893  df-ss 3907  df-nul 4275

This theorem is referenced by:  ssn0  4345  ssdifin0  4426  disjxiun  5083  f1un  6801  fsetexb  8811  infn0  9212  fieq0  9334  infdifsn  9578  cantnff  9595  tc00  9667  hashun3  14346  strleun  17127  dmdprdsplit2lem  20022  2idlval  21249  ocvval  21647  pjfval  21686  opsrle  22025  pf1rcl  22314  en2top  22950  nrmsep  23322  isnrm3  23324  regsep2  23341  xkohaus  23618  kqdisj  23697  regr1lem  23704  alexsublem  24009  reconnlem1  24792  metdstri  24817  iundisj2  25516  left0s  27885  right0s  27886  0clwlk0  30202  disjxpin  32658  iundisj2f  32660  iundisj2fi  32870  1arithufdlem4  33607  cvmsss2  35456  cldbnd  36508  cntotbnd  38117  nna4b4nsq  43093  mapfzcons1  43149  onfrALTlem2  44973  onfrALTlem2VD  45315  nnuzdisj  45785  ssdisjd  49277  ssdisjdr  49278  sepnsepolem2  49392  sepnsepo  49393  resccat  49543