Theorem fvexg 5717

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 2833	. . 3 ⊢ (𝐴 ∈ 𝑊 → 𝐴 ∈ V)
2		fvssunirng 5713	. . 3 ⊢ (𝐴 ∈ V → (𝐹‘𝐴) ⊆ ∪ ran 𝐹)
3	1, 2	syl 14	. 2 ⊢ (𝐴 ∈ 𝑊 → (𝐹‘𝐴) ⊆ ∪ ran 𝐹)
4		rnexg 5049	. . 3 ⊢ (𝐹 ∈ 𝑉 → ran 𝐹 ∈ V)
5		uniexg 4587	. . 3 ⊢ (ran 𝐹 ∈ V → ∪ ran 𝐹 ∈ V)
6	4, 5	syl 14	. 2 ⊢ (𝐹 ∈ 𝑉 → ∪ ran 𝐹 ∈ V)
7		ssexg 4274	. 2 ⊢ (((𝐹‘𝐴) ⊆ ∪ ran 𝐹 ∧ ∪ ran 𝐹 ∈ V) → (𝐹‘𝐴) ∈ V)
8	3, 6, 7	syl2anr 290	1 ⊢ ((𝐹 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) → (𝐹‘𝐴) ∈ V)

This proof depends on syntax axioms:   → wi 4   ∧ wa 104   ∈ wcel 2209  Vcvv 2821   ⊆ wss 3220  ∪ cuni 3935  ran crn 4777  ‘cfv 5380

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-14 2212  ax-ext 2220  ax-sep 4251  ax-pow 4313  ax-pr 4348  ax-un 4580

This proof depends on definitions:  df-bi 117  df-3an 1011  df-tru 1405  df-nf 1514  df-sb 1816  df-eu 2089  df-mo 2090  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-ral 2533  df-rex 2534  df-v 2823  df-un 3224  df-in 3226  df-ss 3233  df-pw 3690  df-sn 3715  df-pr 3716  df-op 3718  df-uni 3936  df-br 4132  df-opab 4194  df-cnv 4784  df-dm 4786  df-rn 4787  df-iota 5340  df-fv 5388

This theorem is used by:  fvex  5718  ovexg  6122  suppval1  6483  suppimacnvfn  6490  suppssrst  6505  suppssrgst  6506  rdgivallem  6656  frecabex  6673  mapsnconst  6981  mapsnend  7104  cc2lem  7639  addvalex  8218  uzennn  10895  seq1g  10922  seqp1g  10925  seqclg  10931  seqm1g  10933  seqfeq4g  10990  lswwrd  11374  ccatlen  11386  ccatval2  11389  ccatvalfn  11392  ccatalpha  11404  eqs1  11419  swrdlen  11447  swrdfv  11448  swrdwrdsymbg  11459  swrdswrd  11500  absval  11790  climmpt  12092  strnfvnd  13431  imasex  13686  imasival  13687  imasbas  13688  imasplusg  13689  imasmulr  13690  imasaddfnlemg  13695  imasaddvallemg  13696  gzsumfzval  13771  gzsumval2  13774  gzsumsplit1r  13775  gzsumwsubmcl  13861  gzsumcl  13864  grpsubval  13911  mulgval  13985  mulgfng  13987  mulgnngzsum  13990  cntrval  14152  prdsex  14280  prdsval  14281  prdsbaslemss  14282  prdsbas  14284  prdsplusgfval  14292  prdsmulrfval  14294  pwsplusgval  14316  pwsmulrval  14317  znval  15081  znle  15082  znbaslemnn  15084  znbas  15089  znzrhval  15092  znzrhfo  15093  znleval  15098  iscnp4  15456  cnpnei  15457  uhgrspansubgrlem  16734  wlkvtxiedg  16803  wlkvtxiedgg  16804  wlk1walkdom  16817  wlklenvclwlk  16831  trlsegvdeglem3  16920  trlsegvdeglem5  16922  eupth2lem3fi  16934  depindlem1  16964