Theorem sseq0 4171

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 3823	. . 3 ⊢ (𝐵 = ∅ → (𝐴 ⊆ 𝐵 ↔ 𝐴 ⊆ ∅))
2		ss0 4170	. . 3 ⊢ (𝐴 ⊆ ∅ → 𝐴 = ∅)
3	1, 2	syl6bi 245	. 2 ⊢ (𝐵 = ∅ → (𝐴 ⊆ 𝐵 → 𝐴 = ∅))
4	3	impcom 397	1 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 = ∅) → 𝐴 = ∅)

Syntax hints:   → wi 4   ∧ wa 385   = wceq 1653   ⊆ wss 3769  ∅c0 4115

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-ext 2777

This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-clab 2786  df-cleq 2792  df-clel 2795  df-nfc 2930  df-v 3387  df-dif 3772  df-in 3776  df-ss 3783  df-nul 4116

This theorem is referenced by:  ssn0  4172  ssdifin0  4244  disjxiun  4840  undom  8290  fieq0  8569  infdifsn  8804  cantnff  8821  tc00  8874  hashun3  13423  strleun  16293  xpsc0  16535  xpsc1  16536  dmdprdsplit2lem  18760  2idlval  19556  opsrle  19798  pf1rcl  20035  ocvval  20336  pjfval  20375  en2top  21118  nrmsep  21490  isnrm3  21492  regsep2  21509  xkohaus  21785  kqdisj  21864  regr1lem  21871  alexsublem  22176  reconnlem1  22957  metdstri  22982  iundisj2  23657  0clwlk0  27476  disjxpin  29918  iundisj2f  29920  iundisj2fi  30074  cvmsss2  31773  cldbnd  32833  cntotbnd  34082  mapfzcons1  38066  onfrALTlem2  39532  onfrALTlem2VD  39885  nnuzdisj  40315