Theorem base0 15912

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

Syntax hints:   = wceq 1483   (/)c0 3915   ` cfv 5888   1c1 9937   Basecbs 15857

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-sbc 3436  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-opab 4713  df-mpt 4730  df-id 5024  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-iota 5851  df-fun 5890  df-fv 5896  df-slot 15861  df-base 15863

This theorem is referenced by:  elbasfv  15920  elbasov  15921  ressbasss  15932  ress0  15934  0cat  16349  oppcbas  16378  fucbas  16620  xpcbas  16818  xpchomfval  16819  xpccofval  16822  0pos  16954  meet0  17137  join0  17138  oduclatb  17144  isipodrs  17161  0g0  17263  frmdplusg  17391  grpn0  17454  grpinvfvi  17463  mulgfvi  17545  symgbas  17800  symgplusg  17809  psgnfval  17920  subcmn  18242  invrfval  18673  scaffval  18881  00lss  18942  00lsp  18981  asclfval  19334  psrbas  19378  psrplusg  19381  psrmulr  19384  resspsrbas  19415  opsrle  19475  00ply1bas  19610  ply1basfvi  19611  ply1plusgfvi  19612  thlbas  20040  dsmmbas2  20081  dsmmfi  20082  matbas0pc  20215  matbas0  20216  matrcl  20218  mdetfval  20392  madufval  20443  mdegfval  23822  uc1pval  23899  mon1pval  23901  dchrrcl  24965  vtxval0  25931  submomnd  29710  suborng  29815  mendbas  37754  mendplusgfval  37755  mendmulrfval  37757  mendvscafval  37760