Theorem sseq0 4369

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

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

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 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-dif 3920  df-ss 3934  df-nul 4300

This theorem is referenced by:  ssn0  4370  ssdifin0  4452  disjxiun  5107  f1un  6823  fsetexb  8840  undomOLD  9034  infn0  9258  fieq0  9379  infdifsn  9617  cantnff  9634  tc00  9708  hashun3  14356  strleun  17134  dmdprdsplit2lem  19984  2idlval  21168  ocvval  21583  pjfval  21622  opsrle  21961  pf1rcl  22243  en2top  22879  nrmsep  23251  isnrm3  23253  regsep2  23270  xkohaus  23547  kqdisj  23626  regr1lem  23633  alexsublem  23938  reconnlem1  24722  metdstri  24747  iundisj2  25457  left0s  27811  right0s  27812  0clwlk0  30068  disjxpin  32524  iundisj2f  32526  iundisj2fi  32727  1arithufdlem4  33525  cvmsss2  35268  cldbnd  36321  cntotbnd  37797  nna4b4nsq  42655  mapfzcons1  42712  onfrALTlem2  44543  onfrALTlem2VD  44885  nnuzdisj  45358  ssdisjd  48800  ssdisjdr  48801  sepnsepolem2  48915  sepnsepo  48916  resccat  49067