Theorem funfvex 5686

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

Syntax hints:   → wi 4   ∧ wa 104  ∃!weu 2080   ∈ wcel 2203  Vcvv 2812   class class class wbr 4108  dom cdm 4748  ℩cio 5309  Fun wfun 5345  ‘cfv 5351

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-14 2206  ax-ext 2214  ax-sep 4227  ax-pow 4286  ax-pr 4321

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-eu 2083  df-mo 2084  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-ral 2525  df-rex 2526  df-v 2814  df-sbc 3042  df-un 3214  df-in 3216  df-ss 3223  df-pw 3670  df-sn 3694  df-pr 3695  df-op 3697  df-uni 3914  df-br 4109  df-opab 4171  df-id 4413  df-cnv 4756  df-co 4757  df-dm 4758  df-iota 5311  df-fun 5353  df-fv 5359

This theorem is referenced by:  fnbrfvb  5714  fvelrnb  5723  funimass4  5726  fvelimab  5732  fniinfv  5734  funfvdm  5739  dmfco  5744  fvco2  5745  eqfnfv  5774  fndmdif  5782  fndmin  5784  fvimacnvi  5791  fvimacnv  5792  funconstss  5795  fniniseg  5797  fniniseg2  5799  fnniniseg2  5800  fvelrn  5807  rexrn  5813  ralrn  5814  dff3im  5821  fmptco  5842  fsn2  5850  funiun  5858  fnressn  5869  resfunexg  5904  eufnfv  5916  funfvima3  5919  rexima  5926  ralima  5927  fniunfv  5934  elunirn  5938  dff13  5940  foeqcnvco  5962  f1eqcocnv  5963  isocnv2  5984  isoini  5990  f1oiso  5998  fnovex  6082  suppssof1  6283  offveqb  6285  1stexg  6360  2ndexg  6361  smoiso  6532  rdgtfr  6604  rdgruledefgg  6605  rdgivallem  6611  frectfr  6630  frecrdg  6638  en1  7038  fundmen  7046  fnfi  7202  ordiso2  7325  cc2lem  7576  climshft2  11984  slotex  13228  strsetsid  13234  ressbas2d  13270  ressbasid  13272  strressid  13273  ressval3d  13274  prdsex  13471  prdsval  13475  prdsbaslemss  13476  prdsbas  13478  prdsplusg  13479  prdsmulr  13480  pwsbas  13494  pwselbasb  13495  pwssnf1o  13500  imasex  13507  imasival  13508  imasbas  13509  imasplusg  13510  imasmulr  13511  imasaddfn  13519  imasaddval  13520  imasaddf  13521  imasmulfn  13522  imasmulval  13523  imasmulf  13524  qusval  13525  qusex  13527  qusaddvallemg  13535  qusaddflemg  13536  qusaddval  13537  qusaddf  13538  qusmulval  13539  qusmulf  13540  xpsfeq  13547  xpsval  13554  ismgm  13559  plusffvalg  13564  grpidvalg  13575  fn0g  13577  fngsum  13590  igsumvalx  13591  gsumfzval  13593  gsumress  13597  gsum0g  13598  issgrp  13605  ismnddef  13620  issubmnd  13644  ress0g  13645  ismhm  13663  mhmex  13664  issubm  13674  0mhm  13688  grppropstrg  13721  grpinvfvalg  13744  grpinvval  13745  grpinvfng  13746  grpsubfvalg  13747  grpsubval  13748  grpressid  13763  grplactfval  13803  qusgrp2  13819  mulgfvalg  13827  mulgval  13828  mulgex  13829  mulgfng  13830  issubg  13879  subgex  13882  issubg2m  13895  isnsg  13908  releqgg  13926  eqgex  13927  eqgfval  13928  eqgen  13933  isghm  13949  ablressid  14041  mgptopng  14062  isrng  14067  rngressid  14087  qusrng  14091  dfur2g  14095  issrg  14098  isring  14133  ringidss  14162  ringressid  14196  qusring2  14199  dvdsrvald  14227  dvdsrex  14232  unitgrp  14250  unitabl  14251  invrfvald  14256  unitlinv  14260  unitrinv  14261  dvrfvald  14267  rdivmuldivd  14278  invrpropdg  14283  dfrhm2  14288  rhmex  14291  rhmunitinv  14312  isnzr2  14318  issubrng  14333  issubrg  14355  subrgugrp  14374  rrgval  14396  isdomn  14404  aprval  14417  aprap  14421  islmod  14426  scaffvalg  14441  rmodislmod  14486  lssex  14489  lsssetm  14491  islssm  14492  islssmg  14493  islss3  14514  lspfval  14523  lspval  14525  lspcl  14526  lspex  14530  sraval  14572  sralemg  14573  srascag  14577  sravscag  14578  sraipg  14579  sraex  14581  rlmsubg  14593  rlmvnegg  14600  ixpsnbasval  14601  lidlex  14608  rspex  14609  lidlss  14611  lidlrsppropdg  14630  qusrhm  14663  mopnset  14687  psrval  14801  fnpsr  14802  psrbasg  14816  psrelbas  14817  psrplusgg  14820  psraddcl  14822  psr0cl  14823  psrnegcl  14825  psr1clfi  14830  mplvalcoe  14832  fnmpl  14835  mplplusgg  14845  vtxvalg  15998  vtxex  16000  eupth2lem3lem6fi  16453