Theorem sseq0 4351

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

Syntax hints:   → wi 4   ∧ wa 398   = wceq 1554   ⊆ wss 3899  ∅c0 4280

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1809  ax-4 1823  ax-5 1924  ax-6 1981  ax-7 2022  ax-8 2138  ax-9 2146  ax-ext 2728

This theorem depends on definitions:  df-bi 209  df-an 399  df-tru 1557  df-fal 1567  df-ex 1794  df-sb 2085  df-clab 2735  df-cleq 2748  df-clel 2831  df-dif 3902  df-ss 3916  df-nul 4281

This theorem is referenced by:  ssn0  4352  ssdifin0  4433  disjxiun  5091  f1un  6816  fsetexb  8834  infn0  9235  fieq0  9357  infdifsn  9602  cantnff  9619  tc00  9691  hashun3  14387  strleun  17169  dmdprdsplit2lem  20063  2idlval  21294  ocvval  21692  pjfval  21731  opsrle  22073  pf1rcl  22385  en2top  23018  nrmsep  23390  isnrm3  23392  regsep2  23409  xkohaus  23686  kqdisj  23765  regr1lem  23772  alexsublem  24077  reconnlem1  24860  metdstri  24885  iundisj2  25584  left0s  27956  right0s  27957  0clwlk0  30273  disjxpin  32730  iundisj2f  32732  iundisj2fi  32942  1arithufdlem4  33697  cvmsss2  35572  cldbnd  36634  cntotbnd  38243  nna4b4nsq  43190  mapfzcons1  43246  onfrALTlem2  45070  onfrALTlem2VD  45412  nnuzdisj  45879  ssdisjd  49377  ssdisjdr  49378  sepnsepolem2  49492  sepnsepo  49493  resccat  49643