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		sseq0b 4356	. 2 ⊢ (𝐵 = ∅ → (𝐴 ⊆ 𝐵 ↔ 𝐴 = ∅))
2	1	biimpac 484	1 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 = ∅) → 𝐴 = ∅)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ⊆ wss 3902  ∅c0 4282

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-dif 3905  df-ss 3919  df-nul 4283

This theorem is used by:  ssn0  4358  ssdifin0  4444  disjxiun  5104  f1un  6842  fsetexb  8868  infn0  9275  fieq0  9394  infdifsn  9639  cantnff  9656  tc00  9728  hashun3  14450  strleun  17253  dmdprdsplit2lem  20178  2idlval  21457  ocvval  21884  pjfval  21923  opsrle  22267  pf1rcl  22578  en2top  23214  nrmsep  23586  isnrm3  23588  regsep2  23605  xkohaus  23883  kqdisj  23962  regr1lem  23969  alexsublem  24274  reconnlem1  25057  metdstri  25082  iundisj2  25781  left0s  28159  right0s  28160  0clwlk0  30603  disjxpin  33063  iundisj2f  33065  iundisj2fi  33270  1arithufdlem4  33959  cvmsss2  35855  cldbnd  36947  cntotbnd  38548  nna4b4nsq  43508  mapfzcons1  43564  onfrALTlem2  45371  onfrALTlem2VD  45713  nnuzdisj  46187  ssdisjd  49738  ssdisjdr  49739  sepnsepolem2  49851  sepnsepo  49852  resccat  50002