Theorem str0 16901

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

Syntax hints:   = wceq 1542  ∅c0 4262  ‘cfv 6432  Slot cslot 16893

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 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2711  ax-sep 5227  ax-nul 5234  ax-pr 5356

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2072  df-mo 2542  df-eu 2571  df-clab 2718  df-cleq 2732  df-clel 2818  df-nfc 2891  df-ral 3071  df-rex 3072  df-rab 3075  df-v 3433  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-nul 4263  df-if 4466  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4846  df-br 5080  df-opab 5142  df-mpt 5163  df-id 5490  df-xp 5596  df-rel 5597  df-cnv 5598  df-co 5599  df-dm 5600  df-iota 6390  df-fun 6434  df-fv 6440  df-slot 16894

This theorem is referenced by:  strfvi  16902  setsnid  16921  setsnidOLD  16922  base0  16928  resseqnbas  16962  resslemOLD  16963  oppchomfval  17434  oppchomfvalOLD  17435  fuchom  17689  fuchomOLD  17690  xpchomfval  17907  xpccofval  17910  oduleval  18018  0pos  18050  0posOLD  18051  frmdplusg  18504  efmndplusg  18530  oppgplusfval  18963  mgpplusg  19735  opprmulfval  19875  sralem  20450  sralemOLD  20451  srasca  20458  srascaOLD  20459  sravsca  20460  sravscaOLD  20461  sraip  20462  zlmlem  20729  zlmlemOLD  20730  zlmvsca  20738  thlle  20914  thlleOLD  20915  thloc  20917  psrplusg  21161  psrmulr  21164  psrvscafval  21170  opsrle  21259  ply1plusgfvi  21424  psr1sca2  21433  ply1sca2  21436  resstopn  22348  tnglem  23807  tnglemOLD  23808  tngds  23822  tngdsOLD  23823  ttglem  27249  ttglemOLD  27250  iedgval0  27421  resvlem  31539  resvlemOLD  31540  mendplusgfval  41019  mendmulrfval  41021  mendsca  41023  mendvscafval  41024