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  7585  climshft2  11999  slotex  13260  strsetsid  13266  ressbas2d  13302  ressbasid  13304  strressid  13305  ressval3d  13306  prdsex  13503  prdsval  13507  prdsbaslemss  13508  prdsbas  13510  prdsplusg  13511  prdsmulr  13512  pwsbas  13526  pwselbasb  13527  pwssnf1o  13532  imasex  13539  imasival  13540  imasbas  13541  imasplusg  13542  imasmulr  13543  imasaddfn  13551  imasaddval  13552  imasaddf  13553  imasmulfn  13554  imasmulval  13555  imasmulf  13556  qusval  13557  qusex  13559  qusaddvallemg  13567  qusaddflemg  13568  qusaddval  13569  qusaddf  13570  qusmulval  13571  qusmulf  13572  xpsfeq  13579  xpsval  13586  ismgm  13591  plusffvalg  13596  grpidvalg  13607  fn0g  13609  fngsum  13622  igsumvalx  13623  gsumfzval  13625  gsumress  13629  gsum0g  13630  issgrp  13637  ismnddef  13652  issubmnd  13676  ress0g  13677  ismhm  13695  mhmex  13696  issubm  13706  0mhm  13720  grppropstrg  13753  grpinvfvalg  13776  grpinvval  13777  grpinvfng  13778  grpsubfvalg  13779  grpsubval  13780  grpressid  13795  grplactfval  13835  qusgrp2  13851  mulgfvalg  13859  mulgval  13860  mulgex  13861  mulgfng  13862  issubg  13911  subgex  13914  issubg2m  13927  isnsg  13940  releqgg  13958  eqgex  13959  eqgfval  13960  eqgen  13965  isghm  13981  ablressid  14073  mgptopng  14094  isrng  14099  rngressid  14119  qusrng  14123  dfur2g  14127  issrg  14130  isring  14165  ringidss  14194  ringressid  14228  qusring2  14231  dvdsrvald  14260  dvdsrex  14265  unitgrp  14283  unitabl  14284  invrfvald  14289  unitlinv  14293  unitrinv  14294  dvrfvald  14300  rdivmuldivd  14311  invrpropdg  14316  dfrhm2  14321  rhmex  14324  rhmunitinv  14345  isnzr2  14351  issubrng  14367  issubrg  14389  subrgugrp  14408  rrgval  14430  isdomn  14438  aprval  14451  aprap  14458  aprprop  14461  islmod  14488  scaffvalg  14503  rmodislmod  14548  lssex  14551  lsssetm  14553  islssm  14554  islssmg  14555  islss3  14576  lspfval  14585  lspval  14587  lspcl  14588  lspex  14592  sraval  14634  sralemg  14635  srascag  14639  sravscag  14640  sraipg  14641  sraex  14643  rlmsubg  14655  rlmvnegg  14662  ixpsnbasval  14663  lidlex  14670  rspex  14671  lidlss  14673  lidlrsppropdg  14692  qusrhm  14725  mopnset  14749  psrval  14863  fnpsr  14864  psrbasg  14878  psrelbas  14879  psrplusgg  14882  psraddcl  14884  psr0cl  14885  psrnegcl  14887  psr1clfi  14892  mplvalcoe  14894  fnmpl  14897  mplplusgg  14907  vtxvalg  16060  vtxex  16062  eupth2lem3lem6fi  16515