Theorem fvexg 5607

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 5603	. . 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 4951	. . 3 |- ( F e. V -> ran F e. _V )
5		uniexg 4493	. . 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 4190	. 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 3855   ran crn 4683   ` cfv 5279

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 4169  ax-pow 4225  ax-pr 4260  ax-un 4487

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 3622  df-sn 3643  df-pr 3644  df-op 3646  df-uni 3856  df-br 4051  df-opab 4113  df-cnv 4690  df-dm 4692  df-rn 4693  df-iota 5240  df-fv 5287

This theorem is referenced by:  fvex  5608  ovexg  5990  rdgivallem  6479  frecabex  6496  mapsnconst  6793  cc2lem  7393  addvalex  7972  uzennn  10598  seq1g  10625  seqp1g  10628  seqclg  10634  seqm1g  10636  seqfeq4g  10693  lswwrd  11057  ccatlen  11069  ccatval2  11072  ccatvalfn  11075  eqs1  11100  swrdlen  11123  swrdfv  11124  swrdwrdsymbg  11135  swrdswrd  11176  absval  11382  climmpt  11681  strnfvnd  12922  prdsex  13171  prdsval  13175  prdsbaslemss  13176  prdsbas  13178  prdsplusgfval  13186  prdsmulrfval  13188  pwsplusgval  13197  pwsmulrval  13198  imasex  13207  imasival  13208  imasbas  13209  imasplusg  13210  imasmulr  13211  imasaddfnlemg  13216  imasaddvallemg  13217  gsumfzval  13293  gsumval2  13299  gsumsplit1r  13300  gsumprval  13301  gsumfzz  13397  gsumwsubmcl  13398  gsumfzcl  13401  grpsubval  13448  mulgval  13528  mulgfng  13530  mulgnngsum  13533  znval  14468  znle  14469  znbaslemnn  14471  znbas  14476  znzrhval  14479  znzrhfo  14480  znleval  14485  iscnp4  14760  cnpnei  14761