Theorem sseq0 4400

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 4009	. . 3 ⊢ (𝐵 = ∅ → (𝐴 ⊆ 𝐵 ↔ 𝐴 ⊆ ∅))
2		ss0 4399	. . 3 ⊢ (𝐴 ⊆ ∅ → 𝐴 = ∅)
3	1, 2	syl6bi 253	. 2 ⊢ (𝐵 = ∅ → (𝐴 ⊆ 𝐵 → 𝐴 = ∅))
4	3	impcom 409	1 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 = ∅) → 𝐴 = ∅)

Syntax hints:   → wi 4   ∧ wa 397   = wceq 1542   ⊆ wss 3949  ∅c0 4323

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-dif 3952  df-in 3956  df-ss 3966  df-nul 4324

This theorem is referenced by:  ssn0  4401  ssdifin0  4486  disjxiun  5146  f1un  6854  fsetexb  8858  undomOLD  9060  infn0  9307  fieq0  9416  infdifsn  9652  cantnff  9669  tc00  9743  hashun3  14344  strleun  17090  dmdprdsplit2lem  19915  2idlval  20858  ocvval  21220  pjfval  21261  opsrle  21602  pf1rcl  21868  en2top  22488  nrmsep  22861  isnrm3  22863  regsep2  22880  xkohaus  23157  kqdisj  23236  regr1lem  23243  alexsublem  23548  reconnlem1  24342  metdstri  24367  iundisj2  25066  left0s  27387  right0s  27388  0clwlk0  29385  disjxpin  31819  iundisj2f  31821  iundisj2fi  32008  cvmsss2  34265  cldbnd  35211  cntotbnd  36664  nna4b4nsq  41402  mapfzcons1  41455  onfrALTlem2  43307  onfrALTlem2VD  43650  nnuzdisj  44065  ssdisjd  47492  ssdisjdr  47493  sepnsepolem2  47555  sepnsepo  47556