Theorem base0 17141

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		baseid 17139	. 2 ⊢ Base = Slot (Base‘ndx)
2	1	str0 17116	1 ⊢ ∅ = (Base‘∅)

Syntax hints:   = wceq 1541  ∅c0 4285  ‘cfv 6492  ndxcnx 17120  Basecbs 17136

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pow 5310  ax-pr 5377  ax-un 7680  ax-cnex 11082  ax-1cn 11084  ax-addcl 11086

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3061  df-reu 3351  df-rab 3400  df-v 3442  df-sbc 3741  df-csb 3850  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-pss 3921  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-iun 4948  df-br 5099  df-opab 5161  df-mpt 5180  df-tr 5206  df-id 5519  df-eprel 5524  df-po 5532  df-so 5533  df-fr 5577  df-we 5579  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-pred 6259  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-ov 7361  df-om 7809  df-2nd 7934  df-frecs 8223  df-wrecs 8254  df-recs 8303  df-rdg 8341  df-nn 12146  df-slot 17109  df-ndx 17121  df-base 17137

This theorem is referenced by:  elbasfv  17142  elbasov  17143  ressbas  17163  ressbasssg  17164  ressbasssOLD  17167  ress0  17170  0cat  17612  oppcbas  17641  fucbas  17887  xpcbas  18101  xpchomfval  18102  xpccofval  18105  0pos  18244  join0  18326  meet0  18327  oduclatb  18430  isipodrs  18460  0g0  18589  frmdplusg  18779  efmndbas  18796  efmndbasabf  18797  efmndplusg  18805  grpn0  18901  grpinvfvi  18912  mulgfvi  19003  psgnfval  19429  subcmn  19766  submomnd  20061  invrfval  20325  suborng  20809  00lss  20892  00lsp  20932  thlbas  21651  dsmmfi  21693  asclfval  21834  psrbas  21889  psrplusg  21892  psrmulr  21898  resspsrbas  21929  opsrle  22002  00ply1bas  22180  ply1basfvi  22181  ply1plusgfvi  22182  matbas0pc  22353  matbas0  22354  matrcl  22356  mdetfval  22530  madufval  22581  mdegfval  26023  uc1pval  26101  mon1pval  26103  dchrrcl  27207  vtxval0  29112  fracbas  33387  mendbas  43418  mendplusgfval  43419  mendmulrfval  43421  mendvscafval  43424  ipolub00  49234  0func  49328  0funcALT  49329  initc  49332  0thinc  49700  initocmd  49910  termolmd  49911