Theorem str0 16133

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

Syntax hints:   = wceq 1632  ∅c0 4058  ‘cfv 6049  Slot cslot 16078

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-8 2141  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-sep 4933  ax-nul 4941  ax-pow 4992  ax-pr 5055

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ral 3055  df-rex 3056  df-rab 3059  df-v 3342  df-sbc 3577  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-nul 4059  df-if 4231  df-sn 4322  df-pr 4324  df-op 4328  df-uni 4589  df-br 4805  df-opab 4865  df-mpt 4882  df-id 5174  df-xp 5272  df-rel 5273  df-cnv 5274  df-co 5275  df-dm 5276  df-iota 6012  df-fun 6051  df-fv 6057  df-slot 16083

This theorem is referenced by:  base0  16134  strfvi  16135  setsnid  16137  resslem  16155  oppchomfval  16595  fuchom  16842  xpchomfval  17040  xpccofval  17043  0pos  17175  oduleval  17352  frmdplusg  17612  oppgplusfval  17998  symgplusg  18029  mgpplusg  18713  opprmulfval  18845  sralem  19399  srasca  19403  sravsca  19404  sraip  19405  psrplusg  19603  psrmulr  19606  psrvscafval  19612  opsrle  19697  ply1plusgfvi  19834  psr1sca2  19843  ply1sca2  19846  zlmlem  20087  zlmvsca  20092  thlle  20263  thloc  20265  resstopn  21212  tnglem  22665  tngds  22673  ttglem  25976  iedgval0  26152  resvlem  30161  mendplusgfval  38275  mendmulrfval  38277  mendsca  38279  mendvscafval  38280