Theorem sseq0 4403

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

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

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 2708

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 2715  df-cleq 2729  df-clel 2816  df-dif 3954  df-ss 3968  df-nul 4334

This theorem is referenced by:  ssn0  4404  ssdifin0  4486  disjxiun  5140  f1un  6868  fsetexb  8904  undomOLD  9100  infn0  9340  fieq0  9461  infdifsn  9697  cantnff  9714  tc00  9788  hashun3  14423  strleun  17194  dmdprdsplit2lem  20065  2idlval  21261  ocvval  21685  pjfval  21726  opsrle  22065  pf1rcl  22353  en2top  22992  nrmsep  23365  isnrm3  23367  regsep2  23384  xkohaus  23661  kqdisj  23740  regr1lem  23747  alexsublem  24052  reconnlem1  24848  metdstri  24873  iundisj2  25584  left0s  27931  right0s  27932  0clwlk0  30151  disjxpin  32601  iundisj2f  32603  iundisj2fi  32799  1arithufdlem4  33575  cvmsss2  35279  cldbnd  36327  cntotbnd  37803  nna4b4nsq  42670  mapfzcons1  42728  onfrALTlem2  44566  onfrALTlem2VD  44909  nnuzdisj  45366  ssdisjd  48727  ssdisjdr  48728  sepnsepolem2  48820  sepnsepo  48821