Theorem sseq0 4378

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ⊆ wss 3926  ∅c0 4308

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-dif 3929  df-ss 3943  df-nul 4309

This theorem is referenced by:  ssn0  4379  ssdifin0  4461  disjxiun  5116  f1un  6838  fsetexb  8878  undomOLD  9074  infn0  9312  fieq0  9433  infdifsn  9671  cantnff  9688  tc00  9762  hashun3  14402  strleun  17176  dmdprdsplit2lem  20028  2idlval  21212  ocvval  21627  pjfval  21666  opsrle  22005  pf1rcl  22287  en2top  22923  nrmsep  23295  isnrm3  23297  regsep2  23314  xkohaus  23591  kqdisj  23670  regr1lem  23677  alexsublem  23982  reconnlem1  24766  metdstri  24791  iundisj2  25502  left0s  27856  right0s  27857  0clwlk0  30113  disjxpin  32569  iundisj2f  32571  iundisj2fi  32774  1arithufdlem4  33562  cvmsss2  35296  cldbnd  36344  cntotbnd  37820  nna4b4nsq  42683  mapfzcons1  42740  onfrALTlem2  44571  onfrALTlem2VD  44913  nnuzdisj  45382  ssdisjd  48786  ssdisjdr  48787  sepnsepolem2  48897  sepnsepo  48898  resccat  49041