Theorem funfvex 5266

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 4976	. 2 ⊢ (𝐹‘𝐴) = (℩𝑦𝐴𝐹𝑦)
2		funfveu 5262	. . 3 ⊢ ((Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹) → ∃!𝑦 𝐴𝐹𝑦)
3		euiotaex 4949	. . 3 ⊢ (∃!𝑦 𝐴𝐹𝑦 → (℩𝑦𝐴𝐹𝑦) ∈ V)
4	2, 3	syl 14	. 2 ⊢ ((Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹) → (℩𝑦𝐴𝐹𝑦) ∈ V)
5	1, 4	syl5eqel 2169	1 ⊢ ((Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹) → (𝐹‘𝐴) ∈ V)

Syntax hints:   → wi 4   ∧ wa 102   ∈ wcel 1434  ∃!weu 1943  Vcvv 2612   class class class wbr 3811  dom cdm 4400  ℩cio 4931  Fun wfun 4962  ‘cfv 4968

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 663  ax-5 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-10 1437  ax-11 1438  ax-i12 1439  ax-bndl 1440  ax-4 1441  ax-14 1446  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2065  ax-sep 3922  ax-pow 3974  ax-pr 3999

This theorem depends on definitions:  df-bi 115  df-3an 922  df-tru 1288  df-nf 1391  df-sb 1688  df-eu 1946  df-mo 1947  df-clab 2070  df-cleq 2076  df-clel 2079  df-nfc 2212  df-ral 2358  df-rex 2359  df-v 2614  df-sbc 2827  df-un 2988  df-in 2990  df-ss 2997  df-pw 3408  df-sn 3428  df-pr 3429  df-op 3431  df-uni 3628  df-br 3812  df-opab 3866  df-id 4083  df-cnv 4408  df-co 4409  df-dm 4410  df-iota 4933  df-fun 4970  df-fv 4976

This theorem is referenced by:  fnbrfvb  5289  fvelrnb  5296  funimass4  5299  fvelimab  5304  fniinfv  5306  funfvdm  5311  dmfco  5316  fvco2  5317  eqfnfv  5341  fndmdif  5348  fndmin  5350  fvimacnvi  5357  fvimacnv  5358  funconstss  5361  fniniseg  5363  fniniseg2  5365  fnniniseg2  5366  rexsupp  5367  fvelrn  5374  rexrn  5380  ralrn  5381  dff3im  5388  fmptco  5405  fsn2  5412  fnressn  5424  resfunexg  5457  eufnfv  5464  funfvima3  5467  rexima  5473  ralima  5474  fniunfv  5480  elunirn  5484  dff13  5486  foeqcnvco  5508  f1eqcocnv  5509  isocnv2  5530  isoini  5535  f1oiso  5543  fnovex  5616  suppssof1  5806  offveqb  5808  1stexg  5872  2ndexg  5873  smoiso  5998  rdgtfr  6070  rdgruledefgg  6071  rdgivallem  6077  frectfr  6096  frecrdg  6104  en1  6445  fundmen  6452  fnfi  6570  ordiso2  6634  climshft2  10518