Theorem funfvex 5497

Description: The value of a function exists. A special case of Corollary 6.13 of [TakeutiZaring] p. 27. (Contributed by Jim Kingdon, 29-Dec-2018.)

Assertion

Ref	Expression
funfvex	⊢ ((Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹) → (𝐹‘𝐴) ∈ V)

Proof of Theorem funfvex

Dummy variable 𝑦 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-fv 5190	. 2 ⊢ (𝐹‘𝐴) = (℩𝑦𝐴𝐹𝑦)
2		funfveu 5493	. . 3 ⊢ ((Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹) → ∃!𝑦 𝐴𝐹𝑦)
3		euiotaex 5163	. . 3 ⊢ (∃!𝑦 𝐴𝐹𝑦 → (℩𝑦𝐴𝐹𝑦) ∈ V)
4	2, 3	syl 14	. 2 ⊢ ((Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹) → (℩𝑦𝐴𝐹𝑦) ∈ V)
5	1, 4	eqeltrid 2251	1 ⊢ ((Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹) → (𝐹‘𝐴) ∈ V)

Syntax hints:   → wi 4   ∧ wa 103  ∃!weu 2013   ∈ wcel 2135  Vcvv 2721   class class class wbr 3976  dom cdm 4598  ℩cio 5145  Fun wfun 5176  ‘cfv 5182

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1434  ax-7 1435  ax-gen 1436  ax-ie1 1480  ax-ie2 1481  ax-8 1491  ax-10 1492  ax-11 1493  ax-i12 1494  ax-bndl 1496  ax-4 1497  ax-17 1513  ax-i9 1517  ax-ial 1521  ax-i5r 1522  ax-14 2138  ax-ext 2146  ax-sep 4094  ax-pow 4147  ax-pr 4181

This theorem depends on definitions:  df-bi 116  df-3an 969  df-tru 1345  df-nf 1448  df-sb 1750  df-eu 2016  df-mo 2017  df-clab 2151  df-cleq 2157  df-clel 2160  df-nfc 2295  df-ral 2447  df-rex 2448  df-v 2723  df-sbc 2947  df-un 3115  df-in 3117  df-ss 3124  df-pw 3555  df-sn 3576  df-pr 3577  df-op 3579  df-uni 3784  df-br 3977  df-opab 4038  df-id 4265  df-cnv 4606  df-co 4607  df-dm 4608  df-iota 5147  df-fun 5184  df-fv 5190

This theorem is referenced by:  fnbrfvb  5521  fvelrnb  5528  funimass4  5531  fvelimab  5536  fniinfv  5538  funfvdm  5543  dmfco  5548  fvco2  5549  eqfnfv  5577  fndmdif  5584  fndmin  5586  fvimacnvi  5593  fvimacnv  5594  funconstss  5597  fniniseg  5599  fniniseg2  5601  fnniniseg2  5602  rexsupp  5603  fvelrn  5610  rexrn  5616  ralrn  5617  dff3im  5624  fmptco  5645  fsn2  5653  fnressn  5665  resfunexg  5700  eufnfv  5709  funfvima3  5712  rexima  5717  ralima  5718  fniunfv  5724  elunirn  5728  dff13  5730  foeqcnvco  5752  f1eqcocnv  5753  isocnv2  5774  isoini  5780  f1oiso  5788  fnovex  5866  suppssof1  6061  offveqb  6063  1stexg  6127  2ndexg  6128  smoiso  6261  rdgtfr  6333  rdgruledefgg  6334  rdgivallem  6340  frectfr  6359  frecrdg  6367  en1  6756  fundmen  6763  fnfi  6893  ordiso2  6991  cc2lem  7198  climshft2  11233  slotex  12358  strsetsid  12364