Theorem base0 14675

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 14639	. 2 |- Base = Slot 1
2	1	str0 14674	1 |- (/) = ( Base ` (/) )

Syntax hints:   = wceq 1399   (/)c0 3711   ` cfv 5496   1c1 9404   Basecbs 14634

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-8 1828  ax-9 1830  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360  ax-sep 4488  ax-nul 4496  ax-pow 4543  ax-pr 4601

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1402  df-ex 1621  df-nf 1625  df-sb 1748  df-eu 2222  df-mo 2223  df-clab 2368  df-cleq 2374  df-clel 2377  df-nfc 2532  df-ne 2579  df-ral 2737  df-rex 2738  df-rab 2741  df-v 3036  df-sbc 3253  df-dif 3392  df-un 3394  df-in 3396  df-ss 3403  df-nul 3712  df-if 3858  df-sn 3945  df-pr 3947  df-op 3951  df-uni 4164  df-br 4368  df-opab 4426  df-mpt 4427  df-id 4709  df-xp 4919  df-rel 4920  df-cnv 4921  df-co 4922  df-dm 4923  df-iota 5460  df-fun 5498  df-fv 5504  df-slot 14638  df-base 14639

This theorem is referenced by:  elbasfv  14683  elbasov  14684  ressbasss  14693  ress0  14695  0cat  15095  oppcbas  15124  fucbas  15366  xpcbas  15564  xpchomfval  15565  xpccofval  15568  0pos  15701  meet0  15884  join0  15885  oduclatb  15891  isipodrs  15908  0g0  16007  frmdplusg  16139  grpn0  16199  grpinvfvi  16208  mulgfvi  16263  symgbas  16522  symgplusg  16531  psgnfval  16642  subcmn  16962  invrfval  17435  scaffval  17643  00lss  17701  00lsp  17740  asclfval  18096  psrbas  18143  psrbasOLD  18144  psrplusg  18147  psrmulr  18150  resspsrbas  18183  opsrle  18253  00ply1bas  18394  ply1basfvi  18395  ply1plusgfvi  18396  thlbas  18818  dsmmbas2  18859  dsmmfi  18860  matbas0pc  18996  matbas0  18997  matrcl  18999  mdetfval  19173  madufval  19224  mdegfval  22545  uc1pval  22625  mon1pval  22627  dchrrcl  23632  submomnd  27853  suborng  27959  mendbas  31301  mendplusgfval  31302  mendmulrfval  31304  mendvscafval  31307