Theorem fvexg 5688

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

Assertion

Ref	Expression
fvexg	⊢ ((𝐹 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) → (𝐹‘𝐴) ∈ V)

Proof of Theorem fvexg

Step	Hyp	Ref	Expression
1		elex 2824	. . 3 ⊢ (𝐴 ∈ 𝑊 → 𝐴 ∈ V)
2		fvssunirng 5684	. . 3 ⊢ (𝐴 ∈ V → (𝐹‘𝐴) ⊆ ∪ ran 𝐹)
3	1, 2	syl 14	. 2 ⊢ (𝐴 ∈ 𝑊 → (𝐹‘𝐴) ⊆ ∪ ran 𝐹)
4		rnexg 5021	. . 3 ⊢ (𝐹 ∈ 𝑉 → ran 𝐹 ∈ V)
5		uniexg 4559	. . 3 ⊢ (ran 𝐹 ∈ V → ∪ ran 𝐹 ∈ V)
6	4, 5	syl 14	. 2 ⊢ (𝐹 ∈ 𝑉 → ∪ ran 𝐹 ∈ V)
7		ssexg 4248	. 2 ⊢ (((𝐹‘𝐴) ⊆ ∪ ran 𝐹 ∧ ∪ ran 𝐹 ∈ V) → (𝐹‘𝐴) ∈ V)
8	3, 6, 7	syl2anr 290	1 ⊢ ((𝐹 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) → (𝐹‘𝐴) ∈ V)

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2203  Vcvv 2812   ⊆ wss 3210  ∪ cuni 3913  ran crn 4749  ‘cfv 5351

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-13 2205  ax-14 2206  ax-ext 2214  ax-sep 4227  ax-pow 4286  ax-pr 4321  ax-un 4553

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-eu 2083  df-mo 2084  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-ral 2525  df-rex 2526  df-v 2814  df-un 3214  df-in 3216  df-ss 3223  df-pw 3670  df-sn 3694  df-pr 3695  df-op 3697  df-uni 3914  df-br 4109  df-opab 4171  df-cnv 4756  df-dm 4758  df-rn 4759  df-iota 5311  df-fv 5359

This theorem is referenced by:  fvex  5689  ovexg  6083  suppval1  6438  suppimacnvfn  6445  suppssrst  6460  suppssrgst  6461  rdgivallem  6611  frecabex  6628  mapsnconst  6928  mapsnend  7051  cc2lem  7576  addvalex  8155  uzennn  10794  seq1g  10821  seqp1g  10824  seqclg  10830  seqm1g  10832  seqfeq4g  10889  lswwrd  11264  ccatlen  11276  ccatval2  11279  ccatvalfn  11282  ccatalpha  11294  eqs1  11309  swrdlen  11337  swrdfv  11338  swrdwrdsymbg  11349  swrdswrd  11390  absval  11679  climmpt  11978  strnfvnd  13221  prdsex  13471  prdsval  13475  prdsbaslemss  13476  prdsbas  13478  prdsplusgfval  13486  prdsmulrfval  13488  pwsplusgval  13497  pwsmulrval  13498  imasex  13507  imasival  13508  imasbas  13509  imasplusg  13510  imasmulr  13511  imasaddfnlemg  13516  imasaddvallemg  13517  gsumfzval  13593  gsumval2  13599  gsumsplit1r  13600  gsumprval  13601  gsumfzz  13697  gsumwsubmcl  13698  gsumfzcl  13701  grpsubval  13748  mulgval  13828  mulgfng  13830  mulgnngsum  13833  znval  14771  znle  14772  znbaslemnn  14774  znbas  14779  znzrhval  14782  znzrhfo  14783  znleval  14788  iscnp4  15070  cnpnei  15071  uhgrspansubgrlem  16258  wlkvtxiedg  16327  wlkvtxiedgg  16328  wlk1walkdom  16341  wlklenvclwlk  16355  trlsegvdeglem3  16444  trlsegvdeglem5  16446  eupth2lem3fi  16458  depindlem1  16488