Theorem sseq0 4353

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 3993	. . 3 ⊢ (𝐵 = ∅ → (𝐴 ⊆ 𝐵 ↔ 𝐴 ⊆ ∅))
2		ss0 4352	. . 3 ⊢ (𝐴 ⊆ ∅ → 𝐴 = ∅)
3	1, 2	syl6bi 255	. 2 ⊢ (𝐵 = ∅ → (𝐴 ⊆ 𝐵 → 𝐴 = ∅))
4	3	impcom 410	1 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 = ∅) → 𝐴 = ∅)

Syntax hints:   → wi 4   ∧ wa 398   = wceq 1537   ⊆ wss 3936  ∅c0 4291

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 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-dif 3939  df-in 3943  df-ss 3952  df-nul 4292

This theorem is referenced by:  ssn0  4354  ssdifin0  4431  disjxiun  5063  undom  8605  fieq0  8885  infdifsn  9120  cantnff  9137  tc00  9190  hashun3  13746  strleun  16591  dmdprdsplit2lem  19167  2idlval  20006  opsrle  20256  pf1rcl  20512  ocvval  20811  pjfval  20850  en2top  21593  nrmsep  21965  isnrm3  21967  regsep2  21984  xkohaus  22261  kqdisj  22340  regr1lem  22347  alexsublem  22652  reconnlem1  23434  metdstri  23459  iundisj2  24150  0clwlk0  27911  disjxpin  30338  iundisj2f  30340  iundisj2fi  30520  cvmsss2  32521  cldbnd  33674  cntotbnd  35089  mapfzcons1  39363  onfrALTlem2  40929  onfrALTlem2VD  41272  nnuzdisj  41672