Theorem sseq0 4356

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ⊆ wss 3905  ∅c0 4286

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-dif 3908  df-ss 3922  df-nul 4287

This theorem is referenced by:  ssn0  4357  ssdifin0  4439  disjxiun  5092  f1un  6788  fsetexb  8798  infn0  9209  fieq0  9330  infdifsn  9572  cantnff  9589  tc00  9663  hashun3  14309  strleun  17086  dmdprdsplit2lem  19944  2idlval  21176  ocvval  21592  pjfval  21631  opsrle  21970  pf1rcl  22252  en2top  22888  nrmsep  23260  isnrm3  23262  regsep2  23279  xkohaus  23556  kqdisj  23635  regr1lem  23642  alexsublem  23947  reconnlem1  24731  metdstri  24756  iundisj2  25466  left0s  27825  right0s  27826  0clwlk0  30094  disjxpin  32550  iundisj2f  32552  iundisj2fi  32753  1arithufdlem4  33494  cvmsss2  35246  cldbnd  36299  cntotbnd  37775  nna4b4nsq  42633  mapfzcons1  42690  onfrALTlem2  44520  onfrALTlem2VD  44862  nnuzdisj  45335  ssdisjd  48780  ssdisjdr  48781  sepnsepolem2  48895  sepnsepo  48896  resccat  49047