Theorem funfvex 5600

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

Syntax hints:   → wi 4   ∧ wa 104  ∃!weu 2055   ∈ wcel 2177  Vcvv 2773   class class class wbr 4047  dom cdm 4679  ℩cio 5235  Fun wfun 5270  ‘cfv 5276

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 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-14 2180  ax-ext 2188  ax-sep 4166  ax-pow 4222  ax-pr 4257

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1485  df-sb 1787  df-eu 2058  df-mo 2059  df-clab 2193  df-cleq 2199  df-clel 2202  df-nfc 2338  df-ral 2490  df-rex 2491  df-v 2775  df-sbc 3000  df-un 3171  df-in 3173  df-ss 3180  df-pw 3619  df-sn 3640  df-pr 3641  df-op 3643  df-uni 3853  df-br 4048  df-opab 4110  df-id 4344  df-cnv 4687  df-co 4688  df-dm 4689  df-iota 5237  df-fun 5278  df-fv 5284

This theorem is referenced by:  fnbrfvb  5626  fvelrnb  5633  funimass4  5636  fvelimab  5642  fniinfv  5644  funfvdm  5649  dmfco  5654  fvco2  5655  eqfnfv  5684  fndmdif  5692  fndmin  5694  fvimacnvi  5701  fvimacnv  5702  funconstss  5705  fniniseg  5707  fniniseg2  5709  fnniniseg2  5710  rexsupp  5711  fvelrn  5718  rexrn  5724  ralrn  5725  dff3im  5732  fmptco  5753  fsn2  5761  funiun  5768  fnressn  5777  resfunexg  5812  eufnfv  5822  funfvima3  5825  rexima  5830  ralima  5831  fniunfv  5838  elunirn  5842  dff13  5844  foeqcnvco  5866  f1eqcocnv  5867  isocnv2  5888  isoini  5894  f1oiso  5902  fnovex  5984  suppssof1  6183  offveqb  6185  1stexg  6260  2ndexg  6261  smoiso  6395  rdgtfr  6467  rdgruledefgg  6468  rdgivallem  6474  frectfr  6493  frecrdg  6501  en1  6898  fundmen  6905  fnfi  7045  ordiso2  7144  cc2lem  7385  climshft2  11661  slotex  12903  strsetsid  12909  ressbas2d  12944  ressbasid  12946  strressid  12947  ressval3d  12948  prdsex  13145  prdsval  13149  prdsbaslemss  13150  prdsbas  13152  prdsplusg  13153  prdsmulr  13154  pwsbas  13168  pwselbasb  13169  pwssnf1o  13174  imasex  13181  imasival  13182  imasbas  13183  imasplusg  13184  imasmulr  13185  imasaddfn  13193  imasaddval  13194  imasaddf  13195  imasmulfn  13196  imasmulval  13197  imasmulf  13198  qusval  13199  qusex  13201  qusaddvallemg  13209  qusaddflemg  13210  qusaddval  13211  qusaddf  13212  qusmulval  13213  qusmulf  13214  xpsfeq  13221  xpsval  13228  ismgm  13233  plusffvalg  13238  grpidvalg  13249  fn0g  13251  fngsum  13264  igsumvalx  13265  gsumfzval  13267  gsumress  13271  gsum0g  13272  issgrp  13279  ismnddef  13294  issubmnd  13318  ress0g  13319  ismhm  13337  mhmex  13338  issubm  13348  0mhm  13362  grppropstrg  13395  grpinvfvalg  13418  grpinvval  13419  grpinvfng  13420  grpsubfvalg  13421  grpsubval  13422  grpressid  13437  grplactfval  13477  qusgrp2  13493  mulgfvalg  13501  mulgval  13502  mulgex  13503  mulgfng  13504  issubg  13553  subgex  13556  issubg2m  13569  isnsg  13582  releqgg  13600  eqgex  13601  eqgfval  13602  eqgen  13607  isghm  13623  ablressid  13715  mgptopng  13735  isrng  13740  rngressid  13760  qusrng  13764  dfur2g  13768  issrg  13771  isring  13806  ringidss  13835  ringressid  13869  qusring2  13872  reldvdsrsrg  13898  dvdsrvald  13899  dvdsrex  13904  unitgrp  13922  unitabl  13923  invrfvald  13928  unitlinv  13932  unitrinv  13933  dvrfvald  13939  rdivmuldivd  13950  invrpropdg  13955  dfrhm2  13960  rhmex  13963  rhmunitinv  13984  isnzr2  13990  issubrng  14005  issubrg  14027  subrgugrp  14046  rrgval  14068  isdomn  14075  aprval  14088  aprap  14092  islmod  14097  scaffvalg  14112  rmodislmod  14157  lssex  14160  lsssetm  14162  islssm  14163  islssmg  14164  islss3  14185  lspfval  14194  lspval  14196  lspcl  14197  lspex  14201  sraval  14243  sralemg  14244  srascag  14248  sravscag  14249  sraipg  14250  sraex  14252  rlmsubg  14264  rlmvnegg  14271  ixpsnbasval  14272  lidlex  14279  rspex  14280  lidlss  14282  lidlrsppropdg  14301  qusrhm  14334  mopnset  14358  psrval  14472  fnpsr  14473  psrbasg  14480  psrelbas  14481  psrplusgg  14484  psraddcl  14486  psr0cl  14487  psrnegcl  14489  psr1clfi  14494  mplvalcoe  14496  fnmpl  14499  mplplusgg  14509  vtxvalg  15659  vtxex  15661