Theorem funfvex 5534

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 F /\ A e. dom F ) -> ( F ` A ) e. _V )

Proof of Theorem funfvex

Dummy variable y is distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-fv 5226	. 2 |- ( F ` A ) = ( iota y A F y )
2		funfveu 5530	. . 3 |- ( ( Fun F /\ A e. dom F ) -> E! y A F y )
3		euiotaex 5196	. . 3 |- ( E! y A F y -> ( iota y A F y ) e. _V )
4	2, 3	syl 14	. 2 |- ( ( Fun F /\ A e. dom F ) -> ( iota y A F y ) e. _V )
5	1, 4	eqeltrid 2264	1 |- ( ( Fun F /\ A e. dom F ) -> ( F ` A ) e. _V )

Syntax hints:   -> wi 4   /\ wa 104   E!weu 2026   e. wcel 2148   _Vcvv 2739   class class class wbr 4005   dom cdm 4628   iotacio 5178   Fun wfun 5212   ` cfv 5218

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-14 2151  ax-ext 2159  ax-sep 4123  ax-pow 4176  ax-pr 4211

This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ral 2460  df-rex 2461  df-v 2741  df-sbc 2965  df-un 3135  df-in 3137  df-ss 3144  df-pw 3579  df-sn 3600  df-pr 3601  df-op 3603  df-uni 3812  df-br 4006  df-opab 4067  df-id 4295  df-cnv 4636  df-co 4637  df-dm 4638  df-iota 5180  df-fun 5220  df-fv 5226

This theorem is referenced by:  fnbrfvb  5558  fvelrnb  5565  funimass4  5568  fvelimab  5574  fniinfv  5576  funfvdm  5581  dmfco  5586  fvco2  5587  eqfnfv  5615  fndmdif  5623  fndmin  5625  fvimacnvi  5632  fvimacnv  5633  funconstss  5636  fniniseg  5638  fniniseg2  5640  fnniniseg2  5641  rexsupp  5642  fvelrn  5649  rexrn  5655  ralrn  5656  dff3im  5663  fmptco  5684  fsn2  5692  fnressn  5704  resfunexg  5739  eufnfv  5749  funfvima3  5752  rexima  5757  ralima  5758  fniunfv  5765  elunirn  5769  dff13  5771  foeqcnvco  5793  f1eqcocnv  5794  isocnv2  5815  isoini  5821  f1oiso  5829  fnovex  5910  suppssof1  6102  offveqb  6104  1stexg  6170  2ndexg  6171  smoiso  6305  rdgtfr  6377  rdgruledefgg  6378  rdgivallem  6384  frectfr  6403  frecrdg  6411  en1  6801  fundmen  6808  fnfi  6938  ordiso2  7036  cc2lem  7267  climshft2  11316  slotex  12491  strsetsid  12497  ressbas2d  12530  strressid  12532  ressval3d  12533  prdsex  12723  imasex  12731  imasival  12732  imasbas  12733  imasplusg  12734  imasmulr  12735  imasaddfn  12743  imasaddval  12744  imasaddf  12745  imasmulfn  12746  imasmulval  12747  imasmulf  12748  qusval  12749  qusaddvallemg  12757  qusaddflemg  12758  qusaddval  12759  qusaddf  12760  qusmulval  12761  qusmulf  12762  xpsfeq  12769  xpsval  12776  ismgm  12781  plusffvalg  12786  grpidvalg  12797  fn0g  12799  issgrp  12814  ismnddef  12824  issubmnd  12848  ress0g  12849  ismhm  12858  issubm  12868  0mhm  12878  grppropstrg  12900  grpinvfvalg  12920  grpinvval  12921  grpinvfng  12922  grpsubfvalg  12923  grpsubval  12924  grpressid  12936  grplactfval  12976  mulgfvalg  12990  mulgval  12991  mulgfng  12992  issubg  13038  subgex  13041  issubg2m  13054  isnsg  13067  releqgg  13085  eqgfval  13086  eqgen  13091  mgptopng  13144  dfur2g  13150  issrg  13153  isring  13188  ringidss  13217  ringressid  13243  reldvdsrsrg  13266  dvdsrvald  13267  dvdsrex  13272  unitgrp  13290  unitabl  13291  invrfvald  13296  unitlinv  13300  unitrinv  13301  dvrfvald  13307  rdivmuldivd  13318  invrpropdg  13323  issubrg  13347  subrgugrp  13366  aprval  13377  aprap  13381  islmod  13386  scaffvalg  13401  rmodislmod  13446  lsssetm  13449  islssm  13450  islss3  13471