Theorem funfvex 5659

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

Syntax hints:   → wi 4   ∧ wa 104  ∃!weu 2078   ∈ wcel 2201  Vcvv 2801   class class class wbr 4089  dom cdm 4727  ℩cio 5286  Fun wfun 5322  ‘cfv 5328

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-14 2204  ax-ext 2212  ax-sep 4208  ax-pow 4266  ax-pr 4301

This theorem depends on definitions:  df-bi 117  df-3an 1006  df-tru 1400  df-nf 1509  df-sb 1810  df-eu 2081  df-mo 2082  df-clab 2217  df-cleq 2223  df-clel 2226  df-nfc 2362  df-ral 2514  df-rex 2515  df-v 2803  df-sbc 3031  df-un 3203  df-in 3205  df-ss 3212  df-pw 3655  df-sn 3676  df-pr 3677  df-op 3679  df-uni 3895  df-br 4090  df-opab 4152  df-id 4392  df-cnv 4735  df-co 4736  df-dm 4737  df-iota 5288  df-fun 5330  df-fv 5336

This theorem is referenced by:  fnbrfvb  5687  fvelrnb  5696  funimass4  5699  fvelimab  5705  fniinfv  5707  funfvdm  5712  dmfco  5717  fvco2  5718  eqfnfv  5747  fndmdif  5755  fndmin  5757  fvimacnvi  5764  fvimacnv  5765  funconstss  5768  fniniseg  5770  fniniseg2  5772  fnniniseg2  5773  rexsupp  5774  fvelrn  5781  rexrn  5787  ralrn  5788  dff3im  5795  fmptco  5816  fsn2  5824  funiun  5832  fnressn  5843  resfunexg  5878  eufnfv  5890  funfvima3  5893  rexima  5900  ralima  5901  fniunfv  5908  elunirn  5912  dff13  5914  foeqcnvco  5936  f1eqcocnv  5937  isocnv2  5958  isoini  5964  f1oiso  5972  fnovex  6056  suppssof1  6258  offveqb  6260  1stexg  6335  2ndexg  6336  smoiso  6473  rdgtfr  6545  rdgruledefgg  6546  rdgivallem  6552  frectfr  6571  frecrdg  6579  en1  6978  fundmen  6986  fnfi  7140  ordiso2  7239  cc2lem  7490  climshft2  11889  slotex  13132  strsetsid  13138  ressbas2d  13174  ressbasid  13176  strressid  13177  ressval3d  13178  prdsex  13375  prdsval  13379  prdsbaslemss  13380  prdsbas  13382  prdsplusg  13383  prdsmulr  13384  pwsbas  13398  pwselbasb  13399  pwssnf1o  13404  imasex  13411  imasival  13412  imasbas  13413  imasplusg  13414  imasmulr  13415  imasaddfn  13423  imasaddval  13424  imasaddf  13425  imasmulfn  13426  imasmulval  13427  imasmulf  13428  qusval  13429  qusex  13431  qusaddvallemg  13439  qusaddflemg  13440  qusaddval  13441  qusaddf  13442  qusmulval  13443  qusmulf  13444  xpsfeq  13451  xpsval  13458  ismgm  13463  plusffvalg  13468  grpidvalg  13479  fn0g  13481  fngsum  13494  igsumvalx  13495  gsumfzval  13497  gsumress  13501  gsum0g  13502  issgrp  13509  ismnddef  13524  issubmnd  13548  ress0g  13549  ismhm  13567  mhmex  13568  issubm  13578  0mhm  13592  grppropstrg  13625  grpinvfvalg  13648  grpinvval  13649  grpinvfng  13650  grpsubfvalg  13651  grpsubval  13652  grpressid  13667  grplactfval  13707  qusgrp2  13723  mulgfvalg  13731  mulgval  13732  mulgex  13733  mulgfng  13734  issubg  13783  subgex  13786  issubg2m  13799  isnsg  13812  releqgg  13830  eqgex  13831  eqgfval  13832  eqgen  13837  isghm  13853  ablressid  13945  mgptopng  13966  isrng  13971  rngressid  13991  qusrng  13995  dfur2g  13999  issrg  14002  isring  14037  ringidss  14066  ringressid  14100  qusring2  14103  dvdsrvald  14131  dvdsrex  14136  unitgrp  14154  unitabl  14155  invrfvald  14160  unitlinv  14164  unitrinv  14165  dvrfvald  14171  rdivmuldivd  14182  invrpropdg  14187  dfrhm2  14192  rhmex  14195  rhmunitinv  14216  isnzr2  14222  issubrng  14237  issubrg  14259  subrgugrp  14278  rrgval  14300  isdomn  14307  aprval  14320  aprap  14324  islmod  14329  scaffvalg  14344  rmodislmod  14389  lssex  14392  lsssetm  14394  islssm  14395  islssmg  14396  islss3  14417  lspfval  14426  lspval  14428  lspcl  14429  lspex  14433  sraval  14475  sralemg  14476  srascag  14480  sravscag  14481  sraipg  14482  sraex  14484  rlmsubg  14496  rlmvnegg  14503  ixpsnbasval  14504  lidlex  14511  rspex  14512  lidlss  14514  lidlrsppropdg  14533  qusrhm  14566  mopnset  14590  psrval  14704  fnpsr  14705  psrbasg  14717  psrelbas  14718  psrplusgg  14721  psraddcl  14723  psr0cl  14724  psrnegcl  14726  psr1clfi  14731  mplvalcoe  14733  fnmpl  14736  mplplusgg  14746  vtxvalg  15896  vtxex  15898  eupth2lem3lem6fi  16351