Theorem str0 17157

Description: All components of the empty set are empty sets. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 7-Dec-2014.)

Hypothesis

Ref	Expression
str0.a	⊢ 𝐹 = Slot 𝐼

Assertion

Ref	Expression
str0	⊢ ∅ = (𝐹‘∅)

Proof of Theorem str0

Step	Hyp	Ref	Expression
1		0ex 5236	. . 3 ⊢ ∅ ∈ V
2		str0.a	. . 3 ⊢ 𝐹 = Slot 𝐼
3	1, 2	strfvn 17154	. 2 ⊢ (𝐹‘∅) = (∅‘𝐼)
4		0fv 6875	. 2 ⊢ (∅‘𝐼) = ∅
5	3, 4	eqtr2i 2764	1 ⊢ ∅ = (𝐹‘∅)

Syntax hints:   = wceq 1547  ∅c0 4268  ‘cfv 6492  Slot cslot 17149

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2712  ax-sep 5225  ax-nul 5235  ax-pr 5369

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2719  df-cleq 2732  df-clel 2815  df-nfc 2889  df-ne 2936  df-ral 3055  df-rex 3065  df-rab 3393  df-v 3434  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4269  df-if 4462  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-br 5080  df-opab 5142  df-mpt 5161  df-id 5520  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-iota 6448  df-fun 6494  df-fv 6500  df-slot 17150

This theorem is referenced by:  strfvi  17158  setsnid  17176  base0  17182  resseqnbas  17210  oppchomfval  17678  fuchom  17929  xpchomfval  18143  xpccofval  18146  oduleval  18253  0pos  18285  frmdplusg  18820  efmndplusg  18846  oppgplusfval  19321  mgpplusg  20123  opprmulfval  20317  sralem  21173  srasca  21177  sravsca  21178  sraip  21179  zlmlem  21498  zlmvsca  21503  thlle  21679  thloc  21681  psrplusg  21919  psrmulr  21924  psrvscafval  21930  opsrle  22030  ply1plusgfvi  22233  psr1sca2  22242  ply1sca2  22245  resstopn  23176  tnglem  24630  tngds  24638  ttglem  28969  iedgval0  29134  resvlem  33423  sn-base0  42992  mendplusgfval  43633  mendmulrfval  43635  mendsca  43637  mendvscafval  43638  catcrcl  49892