Theorem sseq0 4366

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

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

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 2701

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 2708  df-cleq 2721  df-clel 2803  df-dif 3917  df-ss 3931  df-nul 4297

This theorem is referenced by:  ssn0  4367  ssdifin0  4449  disjxiun  5104  f1un  6820  fsetexb  8837  infn0  9251  fieq0  9372  infdifsn  9610  cantnff  9627  tc00  9701  hashun3  14349  strleun  17127  dmdprdsplit2lem  19977  2idlval  21161  ocvval  21576  pjfval  21615  opsrle  21954  pf1rcl  22236  en2top  22872  nrmsep  23244  isnrm3  23246  regsep2  23263  xkohaus  23540  kqdisj  23619  regr1lem  23626  alexsublem  23931  reconnlem1  24715  metdstri  24740  iundisj2  25450  left0s  27804  right0s  27805  0clwlk0  30061  disjxpin  32517  iundisj2f  32519  iundisj2fi  32720  1arithufdlem4  33518  cvmsss2  35261  cldbnd  36314  cntotbnd  37790  nna4b4nsq  42648  mapfzcons1  42705  onfrALTlem2  44536  onfrALTlem2VD  44878  nnuzdisj  45351  ssdisjd  48796  ssdisjdr  48797  sepnsepolem2  48911  sepnsepo  48912  resccat  49063