Theorem str0 17208

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

Syntax hints:   = wceq 1540  ∅c0 4308  ‘cfv 6531  Slot cslot 17200

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pr 5402

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-opab 5182  df-mpt 5202  df-id 5548  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-iota 6484  df-fun 6533  df-fv 6539  df-slot 17201

This theorem is referenced by:  strfvi  17209  setsnid  17227  base0  17233  resseqnbas  17263  oppchomfval  17726  fuchom  17977  xpchomfval  18191  xpccofval  18194  oduleval  18301  0pos  18333  frmdplusg  18832  efmndplusg  18858  oppgplusfval  19331  mgpplusg  20104  opprmulfval  20299  sralem  21134  srasca  21138  sravsca  21139  sraip  21140  zlmlem  21477  zlmvsca  21482  thlle  21657  thloc  21659  psrplusg  21896  psrmulr  21902  psrvscafval  21908  opsrle  22005  ply1plusgfvi  22177  psr1sca2  22186  ply1sca2  22189  resstopn  23124  tnglem  24579  tngds  24587  ttglem  28855  iedgval0  29019  resvlem  33349  sn-base0  42518  mendplusgfval  43205  mendmulrfval  43207  mendsca  43209  mendvscafval  43210