Theorem funfvex 5620

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 5302	. 2 ⊢ (𝐹‘𝐴) = (℩𝑦𝐴𝐹𝑦)
2		funfveu 5616	. . 3 ⊢ ((Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹) → ∃!𝑦 𝐴𝐹𝑦)
3		euiotaex 5271	. . 3 ⊢ (∃!𝑦 𝐴𝐹𝑦 → (℩𝑦𝐴𝐹𝑦) ∈ V)
4	2, 3	syl 14	. 2 ⊢ ((Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹) → (℩𝑦𝐴𝐹𝑦) ∈ V)
5	1, 4	eqeltrid 2296	1 ⊢ ((Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹) → (𝐹‘𝐴) ∈ V)

Syntax hints:   → wi 4   ∧ wa 104  ∃!weu 2057   ∈ wcel 2180  Vcvv 2779   class class class wbr 4062  dom cdm 4696  ℩cio 5252  Fun wfun 5288  ‘cfv 5294

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 713  ax-5 1473  ax-7 1474  ax-gen 1475  ax-ie1 1519  ax-ie2 1520  ax-8 1530  ax-10 1531  ax-11 1532  ax-i12 1533  ax-bndl 1535  ax-4 1536  ax-17 1552  ax-i9 1556  ax-ial 1560  ax-i5r 1561  ax-14 2183  ax-ext 2191  ax-sep 4181  ax-pow 4237  ax-pr 4272

This theorem depends on definitions:  df-bi 117  df-3an 985  df-tru 1378  df-nf 1487  df-sb 1789  df-eu 2060  df-mo 2061  df-clab 2196  df-cleq 2202  df-clel 2205  df-nfc 2341  df-ral 2493  df-rex 2494  df-v 2781  df-sbc 3009  df-un 3181  df-in 3183  df-ss 3190  df-pw 3631  df-sn 3652  df-pr 3653  df-op 3655  df-uni 3868  df-br 4063  df-opab 4125  df-id 4361  df-cnv 4704  df-co 4705  df-dm 4706  df-iota 5254  df-fun 5296  df-fv 5302

This theorem is referenced by:  fnbrfvb  5646  fvelrnb  5654  funimass4  5657  fvelimab  5663  fniinfv  5665  funfvdm  5670  dmfco  5675  fvco2  5676  eqfnfv  5705  fndmdif  5713  fndmin  5715  fvimacnvi  5722  fvimacnv  5723  funconstss  5726  fniniseg  5728  fniniseg2  5730  fnniniseg2  5731  rexsupp  5732  fvelrn  5739  rexrn  5745  ralrn  5746  dff3im  5753  fmptco  5774  fsn2  5782  funiun  5789  fnressn  5798  resfunexg  5833  eufnfv  5843  funfvima3  5846  rexima  5851  ralima  5852  fniunfv  5859  elunirn  5863  dff13  5865  foeqcnvco  5887  f1eqcocnv  5888  isocnv2  5909  isoini  5915  f1oiso  5923  fnovex  6007  suppssof1  6206  offveqb  6208  1stexg  6283  2ndexg  6284  smoiso  6418  rdgtfr  6490  rdgruledefgg  6491  rdgivallem  6497  frectfr  6516  frecrdg  6524  en1  6921  fundmen  6929  fnfi  7071  ordiso2  7170  cc2lem  7420  climshft2  11783  slotex  13025  strsetsid  13031  ressbas2d  13067  ressbasid  13069  strressid  13070  ressval3d  13071  prdsex  13268  prdsval  13272  prdsbaslemss  13273  prdsbas  13275  prdsplusg  13276  prdsmulr  13277  pwsbas  13291  pwselbasb  13292  pwssnf1o  13297  imasex  13304  imasival  13305  imasbas  13306  imasplusg  13307  imasmulr  13308  imasaddfn  13316  imasaddval  13317  imasaddf  13318  imasmulfn  13319  imasmulval  13320  imasmulf  13321  qusval  13322  qusex  13324  qusaddvallemg  13332  qusaddflemg  13333  qusaddval  13334  qusaddf  13335  qusmulval  13336  qusmulf  13337  xpsfeq  13344  xpsval  13351  ismgm  13356  plusffvalg  13361  grpidvalg  13372  fn0g  13374  fngsum  13387  igsumvalx  13388  gsumfzval  13390  gsumress  13394  gsum0g  13395  issgrp  13402  ismnddef  13417  issubmnd  13441  ress0g  13442  ismhm  13460  mhmex  13461  issubm  13471  0mhm  13485  grppropstrg  13518  grpinvfvalg  13541  grpinvval  13542  grpinvfng  13543  grpsubfvalg  13544  grpsubval  13545  grpressid  13560  grplactfval  13600  qusgrp2  13616  mulgfvalg  13624  mulgval  13625  mulgex  13626  mulgfng  13627  issubg  13676  subgex  13679  issubg2m  13692  isnsg  13705  releqgg  13723  eqgex  13724  eqgfval  13725  eqgen  13730  isghm  13746  ablressid  13838  mgptopng  13858  isrng  13863  rngressid  13883  qusrng  13887  dfur2g  13891  issrg  13894  isring  13929  ringidss  13958  ringressid  13992  qusring2  13995  reldvdsrsrg  14021  dvdsrvald  14022  dvdsrex  14027  unitgrp  14045  unitabl  14046  invrfvald  14051  unitlinv  14055  unitrinv  14056  dvrfvald  14062  rdivmuldivd  14073  invrpropdg  14078  dfrhm2  14083  rhmex  14086  rhmunitinv  14107  isnzr2  14113  issubrng  14128  issubrg  14150  subrgugrp  14169  rrgval  14191  isdomn  14198  aprval  14211  aprap  14215  islmod  14220  scaffvalg  14235  rmodislmod  14280  lssex  14283  lsssetm  14285  islssm  14286  islssmg  14287  islss3  14308  lspfval  14317  lspval  14319  lspcl  14320  lspex  14324  sraval  14366  sralemg  14367  srascag  14371  sravscag  14372  sraipg  14373  sraex  14375  rlmsubg  14387  rlmvnegg  14394  ixpsnbasval  14395  lidlex  14402  rspex  14403  lidlss  14405  lidlrsppropdg  14424  qusrhm  14457  mopnset  14481  psrval  14595  fnpsr  14596  psrbasg  14603  psrelbas  14604  psrplusgg  14607  psraddcl  14609  psr0cl  14610  psrnegcl  14612  psr1clfi  14617  mplvalcoe  14619  fnmpl  14622  mplplusgg  14632  vtxvalg  15782  vtxex  15784