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  6792  fsetexb  8802  infn0  9203  fieq0  9325  infdifsn  9567  cantnff  9584  tc00  9656  hashun3  14335  strleun  17116  dmdprdsplit2lem  20011  2idlval  21239  ocvval  21655  pjfval  21694  opsrle  22034  pf1rcl  22323  en2top  22959  nrmsep  23331  isnrm3  23333  regsep2  23350  xkohaus  23627  kqdisj  23706  regr1lem  23713  alexsublem  24018  reconnlem1  24801  metdstri  24826  iundisj2  25525  left0s  27904  right0s  27905  0clwlk0  30222  disjxpin  32678  iundisj2f  32680  iundisj2fi  32890  1arithufdlem4  33627  cvmsss2  35477  cldbnd  36529  cntotbnd  38128  nna4b4nsq  43104  mapfzcons1  43160  onfrALTlem2  44988  onfrALTlem2VD  45330  nnuzdisj  45800  ssdisjd  49280  ssdisjdr  49281  sepnsepolem2  49395  sepnsepo  49396  resccat  49546