Theorem sseq0 4409

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1537   ⊆ wss 3963  ∅c0 4339

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-fal 1550  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-dif 3966  df-ss 3980  df-nul 4340

This theorem is referenced by:  ssn0  4410  ssdifin0  4492  disjxiun  5145  f1un  6869  fsetexb  8903  undomOLD  9099  infn0  9338  fieq0  9459  infdifsn  9695  cantnff  9712  tc00  9786  hashun3  14420  strleun  17191  dmdprdsplit2lem  20080  2idlval  21279  ocvval  21703  pjfval  21744  opsrle  22083  pf1rcl  22369  en2top  23008  nrmsep  23381  isnrm3  23383  regsep2  23400  xkohaus  23677  kqdisj  23756  regr1lem  23763  alexsublem  24068  reconnlem1  24862  metdstri  24887  iundisj2  25598  left0s  27946  right0s  27947  0clwlk0  30161  disjxpin  32608  iundisj2f  32610  iundisj2fi  32805  1arithufdlem4  33555  cvmsss2  35259  cldbnd  36309  cntotbnd  37783  nna4b4nsq  42647  mapfzcons1  42705  onfrALTlem2  44544  onfrALTlem2VD  44887  nnuzdisj  45305  ssdisjd  48656  ssdisjdr  48657  sepnsepolem2  48719  sepnsepo  48720