Theorem fvexg 5608

Description: Evaluating a set function at a set exists. (Contributed by Mario Carneiro and Jim Kingdon, 28-May-2019.)

Assertion

Ref	Expression
fvexg	|- ( ( F e. V /\ A e. W ) -> ( F ` A ) e. _V )

Proof of Theorem fvexg

Step	Hyp	Ref	Expression
1		elex 2785	. . 3 |- ( A e. W -> A e. _V )
2		fvssunirng 5604	. . 3 |- ( A e. _V -> ( F ` A ) C_ U. ran F )
3	1, 2	syl 14	. 2 |- ( A e. W -> ( F ` A ) C_ U. ran F )
4		rnexg 4952	. . 3 |- ( F e. V -> ran F e. _V )
5		uniexg 4494	. . 3 |- ( ran F e. _V -> U. ran F e. _V )
6	4, 5	syl 14	. 2 |- ( F e. V -> U. ran F e. _V )
7		ssexg 4191	. 2 |- ( ( ( F ` A ) C_ U. ran F /\ U. ran F e. _V ) -> ( F ` A ) e. _V )
8	3, 6, 7	syl2anr 290	1 |- ( ( F e. V /\ A e. W ) -> ( F ` A ) e. _V )

Syntax hints:   -> wi 4   /\ wa 104   e. wcel 2177   _Vcvv 2773   C_ wss 3170   U.cuni 3856   ran crn 4684   ` cfv 5280

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-13 2179  ax-14 2180  ax-ext 2188  ax-sep 4170  ax-pow 4226  ax-pr 4261  ax-un 4488

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-un 3174  df-in 3176  df-ss 3183  df-pw 3623  df-sn 3644  df-pr 3645  df-op 3647  df-uni 3857  df-br 4052  df-opab 4114  df-cnv 4691  df-dm 4693  df-rn 4694  df-iota 5241  df-fv 5288

This theorem is referenced by:  fvex  5609  ovexg  5991  rdgivallem  6480  frecabex  6497  mapsnconst  6794  cc2lem  7398  addvalex  7977  uzennn  10603  seq1g  10630  seqp1g  10633  seqclg  10639  seqm1g  10641  seqfeq4g  10698  lswwrd  11062  ccatlen  11074  ccatval2  11077  ccatvalfn  11080  eqs1  11105  swrdlen  11128  swrdfv  11129  swrdwrdsymbg  11140  swrdswrd  11181  absval  11387  climmpt  11686  strnfvnd  12927  prdsex  13176  prdsval  13180  prdsbaslemss  13181  prdsbas  13183  prdsplusgfval  13191  prdsmulrfval  13193  pwsplusgval  13202  pwsmulrval  13203  imasex  13212  imasival  13213  imasbas  13214  imasplusg  13215  imasmulr  13216  imasaddfnlemg  13221  imasaddvallemg  13222  gsumfzval  13298  gsumval2  13304  gsumsplit1r  13305  gsumprval  13306  gsumfzz  13402  gsumwsubmcl  13403  gsumfzcl  13406  grpsubval  13453  mulgval  13533  mulgfng  13535  mulgnngsum  13538  znval  14473  znle  14474  znbaslemnn  14476  znbas  14481  znzrhval  14484  znzrhfo  14485  znleval  14490  iscnp4  14765  cnpnei  14766