Theorem base0 16234

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 16187	. 2 ⊢ Base = Slot 1
2	1	str0 16233	1 ⊢ ∅ = (Base‘∅)

Syntax hints:   = wceq 1653  ∅c0 4113  ‘cfv 6099  1c1 10223  Basecbs 16181

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-8 2159  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-13 2354  ax-ext 2775  ax-sep 4973  ax-nul 4981  ax-pow 5033  ax-pr 5095

This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-3an 1110  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-mo 2590  df-eu 2607  df-clab 2784  df-cleq 2790  df-clel 2793  df-nfc 2928  df-ral 3092  df-rex 3093  df-rab 3096  df-v 3385  df-sbc 3632  df-dif 3770  df-un 3772  df-in 3774  df-ss 3781  df-nul 4114  df-if 4276  df-sn 4367  df-pr 4369  df-op 4373  df-uni 4627  df-br 4842  df-opab 4904  df-mpt 4921  df-id 5218  df-xp 5316  df-rel 5317  df-cnv 5318  df-co 5319  df-dm 5320  df-iota 6062  df-fun 6101  df-fv 6107  df-slot 16185  df-base 16187

This theorem is referenced by:  elbasfv  16242  elbasov  16243  ressbasss  16254  ress0  16256  0cat  16660  oppcbas  16689  fucbas  16931  xpcbas  17130  xpchomfval  17131  xpccofval  17134  0pos  17266  meet0  17449  join0  17450  oduclatb  17456  isipodrs  17473  0g0  17575  frmdplusg  17704  grpn0  17767  grpinvfvi  17776  mulgfvi  17858  symgbas  18109  symgplusg  18118  psgnfval  18230  subcmn  18554  invrfval  18986  scaffval  19196  00lss  19257  00lsp  19299  asclfval  19654  psrbas  19698  psrplusg  19701  psrmulr  19704  resspsrbas  19735  opsrle  19795  00ply1bas  19929  ply1basfvi  19930  ply1plusgfvi  19931  thlbas  20362  dsmmbas2  20403  dsmmfi  20404  matbas0pc  20537  matbas0  20538  matrcl  20540  mdetfval  20715  madufval  20766  mdegfval  24160  uc1pval  24237  mon1pval  24239  dchrrcl  25314  vtxval0  26266  submomnd  30218  suborng  30323  mendbas  38527  mendplusgfval  38528  mendmulrfval  38530  mendvscafval  38533