Theorem base0 16536

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

Syntax hints:   = wceq 1537  ∅c0 4291  ‘cfv 6355  1c1 10538  Basecbs 16483

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5203  ax-nul 5210  ax-pow 5266  ax-pr 5330

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3496  df-sbc 3773  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4839  df-br 5067  df-opab 5129  df-mpt 5147  df-id 5460  df-xp 5561  df-rel 5562  df-cnv 5563  df-co 5564  df-dm 5565  df-iota 6314  df-fun 6357  df-fv 6363  df-slot 16487  df-base 16489

This theorem is referenced by:  elbasfv  16544  elbasov  16545  ressbasss  16556  ress0  16558  0cat  16959  oppcbas  16988  fucbas  17230  xpcbas  17428  xpchomfval  17429  xpccofval  17432  0pos  17564  meet0  17747  join0  17748  oduclatb  17754  isipodrs  17771  0g0  17874  frmdplusg  18019  efmndbas  18036  efmndbasabf  18037  efmndplusg  18045  grpn0  18135  grpinvfvi  18146  mulgfvi  18230  psgnfval  18628  subcmn  18957  invrfval  19423  00lss  19713  00lsp  19753  asclfval  20108  psrbas  20158  psrplusg  20161  psrmulr  20164  resspsrbas  20195  opsrle  20256  00ply1bas  20408  ply1basfvi  20409  ply1plusgfvi  20410  thlbas  20840  dsmmfi  20882  matbas0pc  21018  matbas0  21019  matrcl  21021  mdetfval  21195  madufval  21246  mdegfval  24656  uc1pval  24733  mon1pval  24735  dchrrcl  25816  vtxval0  26824  submomnd  30711  suborng  30888  bj-isrvec  34578  mendbas  39804  mendplusgfval  39805  mendmulrfval  39807  mendvscafval  39810