Theorem str0 17191

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

Syntax hints:   = wceq 1534  ∅c0 4325  ‘cfv 6554  Slot cslot 17183

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2697  ax-sep 5304  ax-nul 5311  ax-pr 5433

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2704  df-cleq 2718  df-clel 2803  df-nfc 2878  df-ne 2931  df-ral 3052  df-rex 3061  df-rab 3420  df-v 3464  df-dif 3950  df-un 3952  df-ss 3964  df-nul 4326  df-if 4534  df-sn 4634  df-pr 4636  df-op 4640  df-uni 4914  df-br 5154  df-opab 5216  df-mpt 5237  df-id 5580  df-xp 5688  df-rel 5689  df-cnv 5690  df-co 5691  df-dm 5692  df-iota 6506  df-fun 6556  df-fv 6562  df-slot 17184

This theorem is referenced by:  strfvi  17192  setsnid  17211  setsnidOLD  17212  base0  17218  resseqnbas  17255  resslemOLD  17256  oppchomfval  17727  oppchomfvalOLD  17728  fuchom  17985  fuchomOLD  17986  xpchomfval  18203  xpccofval  18206  oduleval  18314  0pos  18346  0posOLD  18347  frmdplusg  18844  efmndplusg  18870  oppgplusfval  19342  mgpplusg  20121  opprmulfval  20318  sralem  21154  sralemOLD  21155  srasca  21162  srascaOLD  21163  sravsca  21164  sravscaOLD  21165  sraip  21166  zlmlem  21506  zlmlemOLD  21507  zlmvsca  21515  thlle  21694  thlleOLD  21695  thloc  21697  psrplusg  21945  psrmulr  21951  psrvscafval  21957  opsrle  22054  ply1plusgfvi  22231  psr1sca2  22240  ply1sca2  22243  resstopn  23181  tnglem  24640  tnglemOLD  24641  tngds  24655  tngdsOLD  24656  ttglem  28804  ttglemOLD  28805  iedgval0  28976  resvlem  33205  resvlemOLD  33206  mendplusgfval  42846  mendmulrfval  42848  mendsca  42850  mendvscafval  42851