Theorem str0 17116

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 5252	. . 3 ⊢ ∅ ∈ V
2		str0.a	. . 3 ⊢ 𝐹 = Slot 𝐼
3	1, 2	strfvn 17113	. 2 ⊢ (𝐹‘∅) = (∅‘𝐼)
4		0fv 6875	. 2 ⊢ (∅‘𝐼) = ∅
5	3, 4	eqtr2i 2760	1 ⊢ ∅ = (𝐹‘∅)

Syntax hints:   = wceq 1541  ∅c0 4285  ‘cfv 6492  Slot cslot 17108

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-pr 5377

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  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-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-opab 5161  df-mpt 5180  df-id 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-iota 6448  df-fun 6494  df-fv 6500  df-slot 17109

This theorem is referenced by:  strfvi  17117  setsnid  17135  base0  17141  resseqnbas  17169  oppchomfval  17637  fuchom  17888  xpchomfval  18102  xpccofval  18105  oduleval  18212  0pos  18244  frmdplusg  18779  efmndplusg  18805  oppgplusfval  19277  mgpplusg  20079  opprmulfval  20275  sralem  21128  srasca  21132  sravsca  21133  sraip  21134  zlmlem  21471  zlmvsca  21476  thlle  21652  thloc  21654  psrplusg  21892  psrmulr  21898  psrvscafval  21904  opsrle  22002  ply1plusgfvi  22182  psr1sca2  22191  ply1sca2  22194  resstopn  23130  tnglem  24584  tngds  24592  ttglem  28948  iedgval0  29113  resvlem  33414  sn-base0  42746  mendplusgfval  43419  mendmulrfval  43421  mendsca  43423  mendvscafval  43424  catcrcl  49636