Theorem funfvex 5548

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

Syntax hints:   → wi 4   ∧ wa 104  ∃!weu 2038   ∈ wcel 2160  Vcvv 2752   class class class wbr 4018  dom cdm 4641  ℩cio 5191  Fun wfun 5226  ‘cfv 5232

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 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-14 2163  ax-ext 2171  ax-sep 4136  ax-pow 4189  ax-pr 4224

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1472  df-sb 1774  df-eu 2041  df-mo 2042  df-clab 2176  df-cleq 2182  df-clel 2185  df-nfc 2321  df-ral 2473  df-rex 2474  df-v 2754  df-sbc 2978  df-un 3148  df-in 3150  df-ss 3157  df-pw 3592  df-sn 3613  df-pr 3614  df-op 3616  df-uni 3825  df-br 4019  df-opab 4080  df-id 4308  df-cnv 4649  df-co 4650  df-dm 4651  df-iota 5193  df-fun 5234  df-fv 5240

This theorem is referenced by:  fnbrfvb  5573  fvelrnb  5580  funimass4  5583  fvelimab  5589  fniinfv  5591  funfvdm  5596  dmfco  5601  fvco2  5602  eqfnfv  5630  fndmdif  5638  fndmin  5640  fvimacnvi  5647  fvimacnv  5648  funconstss  5651  fniniseg  5653  fniniseg2  5655  fnniniseg2  5656  rexsupp  5657  fvelrn  5664  rexrn  5670  ralrn  5671  dff3im  5678  fmptco  5699  fsn2  5707  fnressn  5719  resfunexg  5754  eufnfv  5764  funfvima3  5767  rexima  5772  ralima  5773  fniunfv  5780  elunirn  5784  dff13  5786  foeqcnvco  5808  f1eqcocnv  5809  isocnv2  5830  isoini  5836  f1oiso  5844  fnovex  5925  suppssof1  6119  offveqb  6121  1stexg  6187  2ndexg  6188  smoiso  6322  rdgtfr  6394  rdgruledefgg  6395  rdgivallem  6401  frectfr  6420  frecrdg  6428  en1  6818  fundmen  6825  fnfi  6956  ordiso2  7054  cc2lem  7285  climshft2  11334  slotex  12514  strsetsid  12520  ressbas2d  12553  ressbasid  12555  strressid  12556  ressval3d  12557  prdsex  12747  imasex  12755  imasival  12756  imasbas  12757  imasplusg  12758  imasmulr  12759  imasaddfn  12767  imasaddval  12768  imasaddf  12769  imasmulfn  12770  imasmulval  12771  imasmulf  12772  qusval  12773  qusex  12775  qusaddvallemg  12782  qusaddflemg  12783  qusaddval  12784  qusaddf  12785  qusmulval  12786  qusmulf  12787  xpsfeq  12794  xpsval  12801  ismgm  12806  plusffvalg  12811  grpidvalg  12822  fn0g  12824  issgrp  12839  ismnddef  12852  issubmnd  12876  ress0g  12877  ismhm  12886  mhmex  12887  issubm  12897  0mhm  12911  grppropstrg  12937  grpinvfvalg  12959  grpinvval  12960  grpinvfng  12961  grpsubfvalg  12962  grpsubval  12963  grpressid  12978  grplactfval  13018  qusgrp2  13028  mulgfvalg  13036  mulgval  13037  mulgex  13038  mulgfng  13039  issubg  13085  subgex  13088  issubg2m  13101  isnsg  13114  releqgg  13132  eqgex  13133  eqgfval  13134  eqgen  13139  isghm  13150  ablressid  13240  mgptopng  13251  isrng  13256  rngressid  13276  qusrng  13280  dfur2g  13284  issrg  13287  isring  13322  ringidss  13351  ringressid  13381  qusring2  13384  reldvdsrsrg  13410  dvdsrvald  13411  dvdsrex  13416  unitgrp  13434  unitabl  13435  invrfvald  13440  unitlinv  13444  unitrinv  13445  dvrfvald  13451  rdivmuldivd  13462  invrpropdg  13467  dfrhm2  13472  rhmex  13475  rhmunitinv  13496  issubrng  13514  issubrg  13536  subrgugrp  13555  aprval  13566  aprap  13570  islmod  13575  scaffvalg  13590  rmodislmod  13635  lssex  13638  lsssetm  13640  islssm  13641  islssmg  13642  islss3  13663  lspfval  13672  lspval  13674  lspcl  13675  lspex  13679  sraval  13721  sralemg  13722  srascag  13726  sravscag  13727  sraipg  13728  sraex  13730  rlmsubg  13742  rlmvnegg  13749  ixpsnbasval  13750  lidlex  13757  rspex  13758  lidlss  13760  lidlrsppropdg  13779