Theorem funfvex 5715

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 104  ∃!weu 2086   ∈ wcel 2209  Vcvv 2821   class class class wbr 4131  dom cdm 4776  ℩cio 5338  Fun wfun 5374  ‘cfv 5380

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-14 2212  ax-ext 2220  ax-sep 4251  ax-pow 4313  ax-pr 4348

This proof depends on definitions:  df-bi 117  df-3an 1011  df-tru 1405  df-nf 1514  df-sb 1816  df-eu 2089  df-mo 2090  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-ral 2533  df-rex 2534  df-v 2823  df-sbc 3052  df-un 3224  df-in 3226  df-ss 3233  df-pw 3690  df-sn 3715  df-pr 3716  df-op 3718  df-uni 3936  df-br 4132  df-opab 4194  df-id 4440  df-cnv 4784  df-co 4785  df-dm 4786  df-iota 5340  df-fun 5382  df-fv 5388

This theorem is used by:  fnbrfvb  5744  fvelrnb  5753  funimass4  5756  fvelimab  5762  fniinfv  5764  funfvdm  5769  dmfco  5776  fvco2  5777  eqfnfv  5809  fndmdif  5817  fndmin  5819  fvimacnvi  5826  fvimacnv  5827  funconstss  5830  fniniseg  5832  fniniseg2  5834  fnniniseg2  5835  fvelrn  5842  rexrn  5848  ralrn  5849  dff3im  5856  fmptco  5877  fsn2  5885  funiun  5893  fnressn  5904  resfunexg  5939  eufnfv  5952  funfvima3  5955  rexima  5963  ralima  5964  fniunfv  5971  elunirn  5975  dff13  5977  foeqcnvco  5999  f1eqcocnv  6000  isocnv2  6021  isoini  6027  f1oiso  6035  fnovex  6121  suppssof1  6324  offveqb  6326  1stexg  6405  2ndexg  6406  smoiso  6577  rdgtfr  6649  rdgruledefgg  6650  rdgivallem  6656  frectfr  6675  frecrdg  6683  en1  7091  fundmen  7099  fnfi  7255  ordiso2  7382  cc2lem  7639  climshft2  12098  slotex  13438  strsetsid  13444  ressbas2d  13482  ressbasid  13484  strressid  13485  ressval3d  13486  imasex  13686  imasival  13687  imasbas  13688  imasplusg  13689  imasmulr  13690  imasaddfn  13698  imasaddval  13699  imasaddf  13700  imasmulfn  13701  imasmulval  13702  imasmulf  13703  qusval  13704  qusex  13706  qusaddvallemg  13714  qusaddflemg  13715  qusaddval  13716  qusaddf  13717  qusmulval  13718  qusmulf  13719  xpsfeq  13726  ismgm  13737  plusffvalg  13742  grpidvalg  13753  fn0g  13755  fngzsum  13768  gzsumvalx  13769  gzsumfzval  13771  gzsumress  13772  gzsum0  13773  issgrp  13778  ismnddef  13791  issubmnd  13815  ress0g  13816  ismhm  13828  mhmex  13829  issubm  13839  0mhm  13853  grppropstrg  13884  grpinvfvalg  13907  grpinvval  13908  grpinvfng  13909  grpsubfvalg  13910  grpsubval  13911  grpressid  13926  grplactfval  13966  qusgrp2  13976  mulgfvalg  13984  mulgval  13985  mulgex  13986  mulgfng  13987  issubg  14036  subgex  14039  issubg2m  14052  isnsg  14065  releqgg  14083  eqgex  14084  eqgfval  14085  eqgen  14090  isghm  14106  cntzex  14151  cntrval  14152  cntzfval  14153  cntzval  14154  ablressid  14230  prdsex  14280  prdsval  14281  prdsbaslemss  14282  prdsbas  14284  prdsplusg  14285  prdsmulr  14286  xpsval  14309  pwsbas  14313  pwselbasb  14314  pwssnf1o  14319  mgptopng  14336  isrng  14341  rngressid  14361  qusrng  14365  dfur2g  14374  issrg  14377  isring  14412  ringidss  14442  ringressid  14478  qusring2  14481  dvdsrvald  14510  dvdsrex  14515  unitgrp  14533  unitabl  14534  invrfvald  14539  unitlinv  14543  unitrinv  14544  dvrfvald  14550  rdivmuldivd  14561  invrpropdg  14566  dfrhm2  14571  rhmex  14574  rhmunitinv  14595  isnzr2  14601  issubrng  14617  issubrg  14639  subrgugrp  14658  rrgval  14680  isdomn  14688  aprval  14701  aprap  14708  aprprop  14711  islmod  14737  scaffvalg  14753  rmodislmod  14798  lssex  14801  lsssetm  14803  islssm  14804  islssmg  14805  islss3  14826  lspfval  14835  lspval  14837  lspcl  14838  lspex  14842  sraval  14884  sralemg  14885  srascag  14889  sravscag  14890  sraipg  14891  sraex  14893  rlmsubg  14905  rlmvnegg  14912  ixpsnbasval  14913  lidlex  14920  rspex  14921  lidlss  14923  lidlrsppropdg  14942  qusrhm  14975  mopnset  14999  aspval  15125  asclfval  15131  psrval  15162  fnpsr  15163  psrbasg  15183  psrelbas  15184  psrplusgg  15187  psraddcl  15189  psrmulrg  15191  psrmulclfilem  15194  psr0cl  15196  psrnegcl  15198  psr1clfi  15203  psrlidmfi  15204  mvrval2  15212  mvrffi  15214  mplvalcoe  15218  fnmpl  15221  mplplusgg  15231  vtxvalg  16474  vtxex  16476  eupth2lem3lem6fi  16929