Theorem funfvex 5135

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 4853	. 2 |- ( F ` A) = ( iotayA Fy)
2		funfveu 5131	. . 3 |- (( Fun F /\ A e. dom F) -> E!y A Fy)
3		euiotaex 4826	. . 3 |- (E!y A Fy -> ( iotayA Fy) e. _V)
4	2, 3	syl 14	. 2 |- (( Fun F /\ A e. dom F) -> ( iotayA Fy) e. _V)
5	1, 4	syl5eqel 2121	1 |- (( Fun F /\ A e. dom F) -> ( F ` A) e. _V)

Syntax hints:   -> wi 4   /\ wa 97   e. wcel 1390  E!weu 1897   _Vcvv 2551   class class class wbr 3755   dom cdm 4288   iotacio 4808   Fun wfun 4839   ` cfv 4845

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-10 1393  ax-11 1394  ax-i12 1395  ax-bndl 1396  ax-4 1397  ax-14 1402  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019  ax-sep 3866  ax-pow 3918  ax-pr 3935

This theorem depends on definitions:  df-bi 110  df-3an 886  df-tru 1245  df-nf 1347  df-sb 1643  df-eu 1900  df-mo 1901  df-clab 2024  df-cleq 2030  df-clel 2033  df-nfc 2164  df-ral 2305  df-rex 2306  df-v 2553  df-sbc 2759  df-un 2916  df-in 2918  df-ss 2925  df-pw 3353  df-sn 3373  df-pr 3374  df-op 3376  df-uni 3572  df-br 3756  df-opab 3810  df-id 4021  df-cnv 4296  df-co 4297  df-dm 4298  df-iota 4810  df-fun 4847  df-fv 4853

This theorem is referenced by:  fnbrfvb  5157  fvelrnb  5164  funimass4  5167  fvelimab  5172  fniinfv  5174  funfvdm  5179  dmfco  5184  fvco2  5185  eqfnfv  5208  fndmdif  5215  fndmin  5217  fvimacnvi  5224  fvimacnv  5225  funconstss  5228  fniniseg  5230  fniniseg2  5232  fnniniseg2  5233  rexsupp  5234  fvelrn  5241  rexrn  5247  ralrn  5248  dff3im  5255  fmptco  5273  fsn2  5280  fnressn  5292  resfunexg  5325  eufnfv  5332  funfvima3  5335  rexima  5337  ralima  5338  fniunfv  5344  elunirn  5348  dff13  5350  foeqcnvco  5373  f1eqcocnv  5374  isocnv2  5395  isoini  5400  f1oiso  5408  fnovex  5481  suppssof1  5670  offveqb  5672  1stexg  5736  2ndexg  5737  smoiso  5858  rdgtfr  5901  rdgruledefgg  5902  rdgivallem  5908  frectfr  5924  frecrdg  5931  freccl  5932  en1  6215  fundmen  6222