Theorem str0 17118

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

Syntax hints:   = wceq 1540  ∅c0 4286  ‘cfv 6486  Slot cslot 17110

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 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5238  ax-nul 5248  ax-pr 5374

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 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3397  df-v 3440  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-br 5096  df-opab 5158  df-mpt 5177  df-id 5518  df-xp 5629  df-rel 5630  df-cnv 5631  df-co 5632  df-dm 5633  df-iota 6442  df-fun 6488  df-fv 6494  df-slot 17111

This theorem is referenced by:  strfvi  17119  setsnid  17137  base0  17143  resseqnbas  17171  oppchomfval  17638  fuchom  17889  xpchomfval  18103  xpccofval  18106  oduleval  18213  0pos  18245  frmdplusg  18746  efmndplusg  18772  oppgplusfval  19245  mgpplusg  20047  opprmulfval  20242  sralem  21098  srasca  21102  sravsca  21103  sraip  21104  zlmlem  21441  zlmvsca  21446  thlle  21622  thloc  21624  psrplusg  21861  psrmulr  21867  psrvscafval  21873  opsrle  21970  ply1plusgfvi  22142  psr1sca2  22151  ply1sca2  22154  resstopn  23089  tnglem  24544  tngds  24552  ttglem  28839  iedgval0  29003  resvlem  33281  sn-base0  42468  mendplusgfval  43154  mendmulrfval  43156  mendsca  43158  mendvscafval  43159  catcrcl  49381