Theorem sseq0 4330

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1539   ⊆ wss 3883  ∅c0 4253

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-dif 3886  df-in 3890  df-ss 3900  df-nul 4254

This theorem is referenced by:  ssn0  4331  ssdifin0  4413  disjxiun  5067  fsetexb  8610  undom  8800  fieq0  9110  infdifsn  9345  cantnff  9362  tc00  9437  hashun3  14027  strleun  16786  dmdprdsplit2lem  19563  2idlval  20417  ocvval  20784  pjfval  20823  opsrle  21158  pf1rcl  21425  en2top  22043  nrmsep  22416  isnrm3  22418  regsep2  22435  xkohaus  22712  kqdisj  22791  regr1lem  22798  alexsublem  23103  reconnlem1  23895  metdstri  23920  iundisj2  24618  0clwlk0  28397  disjxpin  30828  iundisj2f  30830  iundisj2fi  31020  cvmsss2  33136  left0s  34002  right0s  34003  cldbnd  34442  cntotbnd  35881  nna4b4nsq  40413  mapfzcons1  40455  onfrALTlem2  42055  onfrALTlem2VD  42398  nnuzdisj  42784  ssdisjd  46041  ssdisjdr  46042  sepnsepolem2  46104  sepnsepo  46105