Theorem str0 17150

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

Syntax hints:   = wceq 1542  ∅c0 4274  ‘cfv 6492  Slot cslot 17142

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5231  ax-nul 5241  ax-pr 5370

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-mpt 5168  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 17143

This theorem is referenced by:  strfvi  17151  setsnid  17169  base0  17175  resseqnbas  17203  oppchomfval  17671  fuchom  17922  xpchomfval  18136  xpccofval  18139  oduleval  18246  0pos  18278  frmdplusg  18813  efmndplusg  18839  oppgplusfval  19314  mgpplusg  20116  opprmulfval  20310  sralem  21163  srasca  21167  sravsca  21168  sraip  21169  zlmlem  21506  zlmvsca  21511  thlle  21687  thloc  21689  psrplusg  21926  psrmulr  21931  psrvscafval  21937  opsrle  22035  ply1plusgfvi  22215  psr1sca2  22224  ply1sca2  22227  resstopn  23161  tnglem  24615  tngds  24623  ttglem  28958  iedgval0  29123  resvlem  33408  sn-base0  42954  mendplusgfval  43627  mendmulrfval  43629  mendsca  43631  mendvscafval  43632  catcrcl  49882