Theorem sseq0 4354

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541   ⊆ wss 3899  ∅c0 4284

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-dif 3902  df-ss 3916  df-nul 4285

This theorem is referenced by:  ssn0  4355  ssdifin0  4437  disjxiun  5092  f1un  6791  fsetexb  8797  infn0  9196  fieq0  9315  infdifsn  9557  cantnff  9574  tc00  9646  hashun3  14301  strleun  17078  dmdprdsplit2lem  19969  2idlval  21198  ocvval  21614  pjfval  21653  opsrle  21992  pf1rcl  22274  en2top  22910  nrmsep  23282  isnrm3  23284  regsep2  23301  xkohaus  23578  kqdisj  23657  regr1lem  23664  alexsublem  23969  reconnlem1  24752  metdstri  24777  iundisj2  25487  left0s  27848  right0s  27849  0clwlk0  30123  disjxpin  32579  iundisj2f  32581  iundisj2fi  32790  1arithufdlem4  33523  cvmsss2  35329  cldbnd  36381  cntotbnd  37846  nna4b4nsq  42768  mapfzcons1  42824  onfrALTlem2  44653  onfrALTlem2VD  44995  nnuzdisj  45468  ssdisjd  48922  ssdisjdr  48923  sepnsepolem2  49037  sepnsepo  49038  resccat  49189