Theorem base0 16308

Description: The base set of the empty structure. (Contributed by David A. Wheeler, 7-Jul-2016.)

Assertion

Ref	Expression
base0	⊢ ∅ = (Base‘∅)

Proof of Theorem base0

Step	Hyp	Ref	Expression
1		df-base 16261	. 2 ⊢ Base = Slot 1
2	1	str0 16307	1 ⊢ ∅ = (Base‘∅)

Syntax hints:   = wceq 1601  ∅c0 4141  ‘cfv 6135  1c1 10273  Basecbs 16255

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-8 2109  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754  ax-sep 5017  ax-nul 5025  ax-pow 5077  ax-pr 5138

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-mo 2551  df-eu 2587  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-ral 3095  df-rex 3096  df-rab 3099  df-v 3400  df-sbc 3653  df-dif 3795  df-un 3797  df-in 3799  df-ss 3806  df-nul 4142  df-if 4308  df-sn 4399  df-pr 4401  df-op 4405  df-uni 4672  df-br 4887  df-opab 4949  df-mpt 4966  df-id 5261  df-xp 5361  df-rel 5362  df-cnv 5363  df-co 5364  df-dm 5365  df-iota 6099  df-fun 6137  df-fv 6143  df-slot 16259  df-base 16261

This theorem is referenced by:  elbasfv  16316  elbasov  16317  ressbasss  16328  ress0  16330  0cat  16734  oppcbas  16763  fucbas  17005  xpcbas  17204  xpchomfval  17205  xpccofval  17208  0pos  17340  meet0  17523  join0  17524  oduclatb  17530  isipodrs  17547  0g0  17649  frmdplusg  17778  grpn0  17841  grpinvfvi  17850  mulgfvi  17932  symgbas  18183  symgplusg  18192  psgnfval  18304  subcmn  18628  invrfval  19060  scaffval  19273  00lss  19334  00lsp  19376  asclfval  19731  psrbas  19775  psrplusg  19778  psrmulr  19781  resspsrbas  19812  opsrle  19872  00ply1bas  20006  ply1basfvi  20007  ply1plusgfvi  20008  thlbas  20439  dsmmbas2  20480  dsmmfi  20481  matbas0pc  20619  matbas0  20620  matrcl  20622  mdetfval  20797  madufval  20848  mdegfval  24259  uc1pval  24336  mon1pval  24338  dchrrcl  25417  vtxval0  26387  submomnd  30272  suborng  30377  mendbas  38713  mendplusgfval  38714  mendmulrfval  38716  mendvscafval  38719