Theorem str0 17250

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

Syntax hints:   = wceq 1570  ∅c0 4287  ‘cfv 6538  Slot cslot 17242

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5258  ax-nul 5270  ax-pr 5406

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4489  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4874  df-br 5111  df-opab 5175  df-mpt 5194  df-id 5558  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-iota 6494  df-fun 6540  df-fv 6546  df-slot 17243

This theorem is referenced by:  strfvi  17251  setsnid  17269  base0  17275  resseqnbas  17303  oppchomfval  17771  fuchom  18022  xpchomfval  18236  xpccofval  18239  oduleval  18346  0pos  18378  frmdplusg  18914  efmndplusg  18940  oppgplusfval  19419  mgpplusg  20221  opprmulfval  20422  sralem  21278  srasca  21282  sravsca  21283  sraip  21284  zlmlem  21647  zlmvsca  21652  thlle  21828  thloc  21830  psrplusg  22068  psrmulr  22073  psrvscafval  22079  opsrle  22179  ply1plusgfvi  22382  psr1sca2  22391  ply1sca2  22394  resstopn  23324  tnglem  24778  tngds  24786  ttglem  29206  iedgval0  29371  resvlem  33634  sn-base0  43250  mendplusgfval  43891  mendmulrfval  43893  mendsca  43895  mendvscafval  43896  catcrcl  50156