Theorem funfvex 5689

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

Syntax hints:   → wi 4   ∧ wa 104  ∃!weu 2082   ∈ wcel 2205  Vcvv 2815   class class class wbr 4111  dom cdm 4751  ℩cio 5312  Fun wfun 5348  ‘cfv 5354

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 2208  ax-ext 2216  ax-sep 4230  ax-pow 4289  ax-pr 4324

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-eu 2085  df-mo 2086  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-ral 2527  df-rex 2528  df-v 2817  df-sbc 3045  df-un 3217  df-in 3219  df-ss 3226  df-pw 3673  df-sn 3697  df-pr 3698  df-op 3700  df-uni 3917  df-br 4112  df-opab 4174  df-id 4416  df-cnv 4759  df-co 4760  df-dm 4761  df-iota 5314  df-fun 5356  df-fv 5362

This theorem is referenced by:  fnbrfvb  5717  fvelrnb  5726  funimass4  5729  fvelimab  5735  fniinfv  5737  funfvdm  5742  dmfco  5747  fvco2  5748  eqfnfv  5777  fndmdif  5785  fndmin  5787  fvimacnvi  5794  fvimacnv  5795  funconstss  5798  fniniseg  5800  fniniseg2  5802  fnniniseg2  5803  fvelrn  5810  rexrn  5816  ralrn  5817  dff3im  5824  fmptco  5845  fsn2  5853  funiun  5861  fnressn  5872  resfunexg  5907  eufnfv  5919  funfvima3  5922  rexima  5929  ralima  5930  fniunfv  5937  elunirn  5941  dff13  5943  foeqcnvco  5965  f1eqcocnv  5966  isocnv2  5987  isoini  5993  f1oiso  6001  fnovex  6085  suppssof1  6286  offveqb  6288  1stexg  6363  2ndexg  6364  smoiso  6535  rdgtfr  6607  rdgruledefgg  6608  rdgivallem  6614  frectfr  6633  frecrdg  6641  en1  7041  fundmen  7049  fnfi  7205  ordiso2  7328  cc2lem  7582  climshft2  11995  slotex  13256  strsetsid  13262  ressbas2d  13298  ressbasid  13300  strressid  13301  ressval3d  13302  prdsex  13499  prdsval  13503  prdsbaslemss  13504  prdsbas  13506  prdsplusg  13507  prdsmulr  13508  pwsbas  13522  pwselbasb  13523  pwssnf1o  13528  imasex  13535  imasival  13536  imasbas  13537  imasplusg  13538  imasmulr  13539  imasaddfn  13547  imasaddval  13548  imasaddf  13549  imasmulfn  13550  imasmulval  13551  imasmulf  13552  qusval  13553  qusex  13555  qusaddvallemg  13563  qusaddflemg  13564  qusaddval  13565  qusaddf  13566  qusmulval  13567  qusmulf  13568  xpsfeq  13575  xpsval  13582  ismgm  13587  plusffvalg  13592  grpidvalg  13603  fn0g  13605  fngsum  13618  igsumvalx  13619  gsumfzval  13621  gsumress  13625  gsum0g  13626  issgrp  13633  ismnddef  13648  issubmnd  13672  ress0g  13673  ismhm  13691  mhmex  13692  issubm  13702  0mhm  13716  grppropstrg  13749  grpinvfvalg  13772  grpinvval  13773  grpinvfng  13774  grpsubfvalg  13775  grpsubval  13776  grpressid  13791  grplactfval  13831  qusgrp2  13847  mulgfvalg  13855  mulgval  13856  mulgex  13857  mulgfng  13858  issubg  13907  subgex  13910  issubg2m  13923  isnsg  13936  releqgg  13954  eqgex  13955  eqgfval  13956  eqgen  13961  isghm  13977  ablressid  14069  mgptopng  14090  isrng  14095  rngressid  14115  qusrng  14119  dfur2g  14123  issrg  14126  isring  14161  ringidss  14190  ringressid  14224  qusring2  14227  dvdsrvald  14255  dvdsrex  14260  unitgrp  14278  unitabl  14279  invrfvald  14284  unitlinv  14288  unitrinv  14289  dvrfvald  14295  rdivmuldivd  14306  invrpropdg  14311  dfrhm2  14316  rhmex  14319  rhmunitinv  14340  isnzr2  14346  issubrng  14361  issubrg  14383  subrgugrp  14402  rrgval  14424  isdomn  14432  aprval  14445  aprap  14449  islmod  14456  scaffvalg  14471  rmodislmod  14516  lssex  14519  lsssetm  14521  islssm  14522  islssmg  14523  islss3  14544  lspfval  14553  lspval  14555  lspcl  14556  lspex  14560  sraval  14602  sralemg  14603  srascag  14607  sravscag  14608  sraipg  14609  sraex  14611  rlmsubg  14623  rlmvnegg  14630  ixpsnbasval  14631  lidlex  14638  rspex  14639  lidlss  14641  lidlrsppropdg  14660  qusrhm  14693  mopnset  14717  psrval  14831  fnpsr  14832  psrbasg  14846  psrelbas  14847  psrplusgg  14850  psraddcl  14852  psr0cl  14853  psrnegcl  14855  psr1clfi  14860  mplvalcoe  14862  fnmpl  14865  mplplusgg  14875  vtxvalg  16028  vtxex  16030  eupth2lem3lem6fi  16483