Theorem sseq0 4357

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		sseq0b 4356	. 2 ⊢ (𝐵 = ∅ → (𝐴 ⊆ 𝐵 ↔ 𝐴 = ∅))
2	1	biimpac 484	1 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 = ∅) → 𝐴 = ∅)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ⊆ wss 3900  ∅c0 4281

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ss 3901  df-dif 4050  df-nul 4282

This theorem is used by:  ssn0  4358  ssdifin0  4444  disjxiun  5103  f1un  6867  fsetexb  8914  infn0  9322  fieq0  9440  infdifsn  9685  cantnff  9702  tc00  9774  hashun3  14555  strleun  17364  dmdprdsplit2lem  20291  2idlval  21574  ocvval  22003  pjfval  22042  opsrle  22386  pf1rcl  22697  en2top  23333  nrmsep  23705  isnrm3  23707  regsep2  23724  xkohaus  24002  kqdisj  24081  regr1lem  24088  alexsublem  24393  reconnlem1  25176  metdstri  25201  iundisj2  25900  left0s  28309  right0s  28310  0clwlk0  30753  disjxpin  33254  iundisj2f  33256  iundisj2fi  33459  1arithufdlem4  34149  cvmsss2  36206  cldbnd  37292  cntotbnd  38922  mapfzcons1  43921  onfrALTlem2  45720  onfrALTlem2VD  46062  nnuzdisj  46572  ssdisjd  50123  ssdisjdr  50124  sepnsepolem2  50242  sepnsepo  50243  resccat  50393