Theorem funfvex 5692

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 5365	. 2 ⊢ (𝐹‘𝐴) = (℩𝑦𝐴𝐹𝑦)
2		funfveu 5688	. . 3 ⊢ ((Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹) → ∃!𝑦 𝐴𝐹𝑦)
3		euiotaex 5334	. . 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 4114  dom cdm 4754  ℩cio 5315  Fun wfun 5351  ‘cfv 5357

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 4233  ax-pow 4292  ax-pr 4327

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 3046  df-un 3218  df-in 3220  df-ss 3227  df-pw 3676  df-sn 3700  df-pr 3701  df-op 3703  df-uni 3920  df-br 4115  df-opab 4177  df-id 4419  df-cnv 4762  df-co 4763  df-dm 4764  df-iota 5317  df-fun 5359  df-fv 5365

This theorem is referenced by:  fnbrfvb  5720  fvelrnb  5729  funimass4  5732  fvelimab  5738  fniinfv  5740  funfvdm  5745  dmfco  5750  fvco2  5751  eqfnfv  5780  fndmdif  5788  fndmin  5790  fvimacnvi  5797  fvimacnv  5798  funconstss  5801  fniniseg  5803  fniniseg2  5805  fnniniseg2  5806  fvelrn  5813  rexrn  5819  ralrn  5820  dff3im  5827  fmptco  5848  fsn2  5856  funiun  5864  fnressn  5875  resfunexg  5910  eufnfv  5922  funfvima3  5925  rexima  5933  ralima  5934  fniunfv  5941  elunirn  5945  dff13  5947  foeqcnvco  5969  f1eqcocnv  5970  isocnv2  5991  isoini  5997  f1oiso  6005  fnovex  6091  suppssof1  6293  offveqb  6295  1stexg  6374  2ndexg  6375  smoiso  6546  rdgtfr  6618  rdgruledefgg  6619  rdgivallem  6625  frectfr  6644  frecrdg  6652  en1  7052  fundmen  7060  fnfi  7216  ordiso2  7339  cc2lem  7596  climshft2  12019  slotex  13326  strsetsid  13332  ressbas2d  13368  ressbasid  13370  strressid  13371  ressval3d  13372  imasex  13572  imasival  13573  imasbas  13574  imasplusg  13575  imasmulr  13576  imasaddfn  13584  imasaddval  13585  imasaddf  13586  imasmulfn  13587  imasmulval  13588  imasmulf  13589  qusval  13590  qusex  13592  qusaddvallemg  13600  qusaddflemg  13601  qusaddval  13602  qusaddf  13603  qusmulval  13604  qusmulf  13605  xpsfeq  13612  ismgm  13623  plusffvalg  13628  grpidvalg  13639  fn0g  13641  fngsum  13654  igsumvalx  13655  gsumfzval  13657  gsumress  13661  gsum0g  13662  issgrp  13669  ismnddef  13682  issubmnd  13706  ress0g  13707  ismhm  13719  mhmex  13720  issubm  13730  0mhm  13744  grppropstrg  13777  grpinvfvalg  13800  grpinvval  13801  grpinvfng  13802  grpsubfvalg  13803  grpsubval  13804  grpressid  13819  grplactfval  13859  qusgrp2  13869  mulgfvalg  13877  mulgval  13878  mulgex  13879  mulgfng  13880  issubg  13929  subgex  13932  issubg2m  13945  isnsg  13958  releqgg  13976  eqgex  13977  eqgfval  13978  eqgen  13983  isghm  13999  ablressid  14091  prdsex  14117  prdsval  14118  prdsbaslemss  14119  prdsbas  14121  prdsplusg  14122  prdsmulr  14123  xpsval  14146  pwsbas  14150  pwselbasb  14151  pwssnf1o  14156  mgptopng  14171  isrng  14176  rngressid  14196  qusrng  14200  dfur2g  14208  issrg  14211  isring  14246  ringidss  14275  ringressid  14309  qusring2  14312  dvdsrvald  14341  dvdsrex  14346  unitgrp  14364  unitabl  14365  invrfvald  14370  unitlinv  14374  unitrinv  14375  dvrfvald  14381  rdivmuldivd  14392  invrpropdg  14397  dfrhm2  14402  rhmex  14405  rhmunitinv  14426  isnzr2  14432  issubrng  14448  issubrg  14470  subrgugrp  14489  rrgval  14511  isdomn  14519  aprval  14532  aprap  14539  aprprop  14542  islmod  14568  scaffvalg  14583  rmodislmod  14628  lssex  14631  lsssetm  14633  islssm  14634  islssmg  14635  islss3  14656  lspfval  14665  lspval  14667  lspcl  14668  lspex  14672  sraval  14714  sralemg  14715  srascag  14719  sravscag  14720  sraipg  14721  sraex  14723  rlmsubg  14735  rlmvnegg  14742  ixpsnbasval  14743  lidlex  14750  rspex  14751  lidlss  14753  lidlrsppropdg  14772  qusrhm  14805  mopnset  14829  psrval  14943  fnpsr  14944  psrbasg  14958  psrelbas  14959  psrplusgg  14962  psraddcl  14964  psr0cl  14965  psrnegcl  14967  psr1clfi  14972  mplvalcoe  14974  fnmpl  14977  mplplusgg  14987  vtxvalg  16140  vtxex  16142  eupth2lem3lem6fi  16595