Theorem sseq0 4345

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 3957	. . 3 ⊢ (𝐵 = ∅ → (𝐴 ⊆ 𝐵 ↔ 𝐴 ⊆ ∅))
2		ss0 4344	. . 3 ⊢ (𝐴 ⊆ ∅ → 𝐴 = ∅)
3	1, 2	syl6bi 252	. 2 ⊢ (𝐵 = ∅ → (𝐴 ⊆ 𝐵 → 𝐴 = ∅))
4	3	impcom 408	1 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 = ∅) → 𝐴 = ∅)

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1540   ⊆ wss 3897  ∅c0 4268

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2707

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1543  df-fal 1553  df-ex 1781  df-sb 2067  df-clab 2714  df-cleq 2728  df-clel 2814  df-v 3443  df-dif 3900  df-in 3904  df-ss 3914  df-nul 4269

This theorem is referenced by:  ssn0  4346  ssdifin0  4429  disjxiun  5086  f1un  6781  fsetexb  8715  undomOLD  8917  infn0  9164  fieq0  9270  infdifsn  9506  cantnff  9523  tc00  9597  hashun3  14191  strleun  16947  dmdprdsplit2lem  19735  2idlval  20602  ocvval  20970  pjfval  21011  opsrle  21346  pf1rcl  21613  en2top  22233  nrmsep  22606  isnrm3  22608  regsep2  22625  xkohaus  22902  kqdisj  22981  regr1lem  22988  alexsublem  23293  reconnlem1  24087  metdstri  24112  iundisj2  24811  0clwlk0  28725  disjxpin  31155  iundisj2f  31157  iundisj2fi  31346  cvmsss2  33476  left0s  34166  right0s  34167  cldbnd  34606  cntotbnd  36052  nna4b4nsq  40747  mapfzcons1  40789  onfrALTlem2  42476  onfrALTlem2VD  42819  nnuzdisj  43218  ssdisjd  46493  ssdisjdr  46494  sepnsepolem2  46556  sepnsepo  46557