Theorem funfvex 5649

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

Syntax hints:   → wi 4   ∧ wa 104  ∃!weu 2077   ∈ wcel 2200  Vcvv 2799   class class class wbr 4083  dom cdm 4720  ℩cio 5279  Fun wfun 5315  ‘cfv 5321

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-14 2203  ax-ext 2211  ax-sep 4202  ax-pow 4259  ax-pr 4294

This theorem depends on definitions:  df-bi 117  df-3an 1004  df-tru 1398  df-nf 1507  df-sb 1809  df-eu 2080  df-mo 2081  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ral 2513  df-rex 2514  df-v 2801  df-sbc 3029  df-un 3201  df-in 3203  df-ss 3210  df-pw 3651  df-sn 3672  df-pr 3673  df-op 3675  df-uni 3889  df-br 4084  df-opab 4146  df-id 4385  df-cnv 4728  df-co 4729  df-dm 4730  df-iota 5281  df-fun 5323  df-fv 5329

This theorem is referenced by:  fnbrfvb  5677  fvelrnb  5686  funimass4  5689  fvelimab  5695  fniinfv  5697  funfvdm  5702  dmfco  5707  fvco2  5708  eqfnfv  5737  fndmdif  5745  fndmin  5747  fvimacnvi  5754  fvimacnv  5755  funconstss  5758  fniniseg  5760  fniniseg2  5762  fnniniseg2  5763  rexsupp  5764  fvelrn  5771  rexrn  5777  ralrn  5778  dff3im  5785  fmptco  5806  fsn2  5814  funiun  5821  fnressn  5832  resfunexg  5867  eufnfv  5877  funfvima3  5880  rexima  5887  ralima  5888  fniunfv  5895  elunirn  5899  dff13  5901  foeqcnvco  5923  f1eqcocnv  5924  isocnv2  5945  isoini  5951  f1oiso  5959  fnovex  6043  suppssof1  6245  offveqb  6247  1stexg  6322  2ndexg  6323  smoiso  6459  rdgtfr  6531  rdgruledefgg  6532  rdgivallem  6538  frectfr  6557  frecrdg  6565  en1  6964  fundmen  6972  fnfi  7119  ordiso2  7218  cc2lem  7468  climshft2  11838  slotex  13080  strsetsid  13086  ressbas2d  13122  ressbasid  13124  strressid  13125  ressval3d  13126  prdsex  13323  prdsval  13327  prdsbaslemss  13328  prdsbas  13330  prdsplusg  13331  prdsmulr  13332  pwsbas  13346  pwselbasb  13347  pwssnf1o  13352  imasex  13359  imasival  13360  imasbas  13361  imasplusg  13362  imasmulr  13363  imasaddfn  13371  imasaddval  13372  imasaddf  13373  imasmulfn  13374  imasmulval  13375  imasmulf  13376  qusval  13377  qusex  13379  qusaddvallemg  13387  qusaddflemg  13388  qusaddval  13389  qusaddf  13390  qusmulval  13391  qusmulf  13392  xpsfeq  13399  xpsval  13406  ismgm  13411  plusffvalg  13416  grpidvalg  13427  fn0g  13429  fngsum  13442  igsumvalx  13443  gsumfzval  13445  gsumress  13449  gsum0g  13450  issgrp  13457  ismnddef  13472  issubmnd  13496  ress0g  13497  ismhm  13515  mhmex  13516  issubm  13526  0mhm  13540  grppropstrg  13573  grpinvfvalg  13596  grpinvval  13597  grpinvfng  13598  grpsubfvalg  13599  grpsubval  13600  grpressid  13615  grplactfval  13655  qusgrp2  13671  mulgfvalg  13679  mulgval  13680  mulgex  13681  mulgfng  13682  issubg  13731  subgex  13734  issubg2m  13747  isnsg  13760  releqgg  13778  eqgex  13779  eqgfval  13780  eqgen  13785  isghm  13801  ablressid  13893  mgptopng  13913  isrng  13918  rngressid  13938  qusrng  13942  dfur2g  13946  issrg  13949  isring  13984  ringidss  14013  ringressid  14047  qusring2  14050  dvdsrvald  14078  dvdsrex  14083  unitgrp  14101  unitabl  14102  invrfvald  14107  unitlinv  14111  unitrinv  14112  dvrfvald  14118  rdivmuldivd  14129  invrpropdg  14134  dfrhm2  14139  rhmex  14142  rhmunitinv  14163  isnzr2  14169  issubrng  14184  issubrg  14206  subrgugrp  14225  rrgval  14247  isdomn  14254  aprval  14267  aprap  14271  islmod  14276  scaffvalg  14291  rmodislmod  14336  lssex  14339  lsssetm  14341  islssm  14342  islssmg  14343  islss3  14364  lspfval  14373  lspval  14375  lspcl  14376  lspex  14380  sraval  14422  sralemg  14423  srascag  14427  sravscag  14428  sraipg  14429  sraex  14431  rlmsubg  14443  rlmvnegg  14450  ixpsnbasval  14451  lidlex  14458  rspex  14459  lidlss  14461  lidlrsppropdg  14480  qusrhm  14513  mopnset  14537  psrval  14651  fnpsr  14652  psrbasg  14659  psrelbas  14660  psrplusgg  14663  psraddcl  14665  psr0cl  14666  psrnegcl  14668  psr1clfi  14673  mplvalcoe  14675  fnmpl  14678  mplplusgg  14688  vtxvalg  15838  vtxex  15840