Theorem fexd 7182

Description: If the domain of a mapping is a set, the function is a set. (Contributed by Glauco Siliprandi, 26-Jun-2021.)

Hypotheses

Ref	Expression
fexd.1	⊢ (𝜑 → 𝐹:𝐴⟶𝐵)
fexd.2	⊢ (𝜑 → 𝐴 ∈ 𝐶)

Assertion

Ref	Expression
fexd	⊢ (𝜑 → 𝐹 ∈ V)

Proof of Theorem fexd

Step	Hyp	Ref	Expression
1		fexd.1	. 2 ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)
2		fexd.2	. 2 ⊢ (𝜑 → 𝐴 ∈ 𝐶)
3		fex 7181	. 2 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐴 ∈ 𝐶) → 𝐹 ∈ V)
4	1, 2, 3	syl2anc 585	1 ⊢ (𝜑 → 𝐹 ∈ V)

Syntax hints:   → wi 4   ∈ wcel 2114  Vcvv 3429  ⟶wf 6494

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2708  ax-rep 5212  ax-sep 5231  ax-nul 5241  ax-pr 5375

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3062  df-reu 3343  df-rab 3390  df-v 3431  df-sbc 3729  df-csb 3838  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-iun 4935  df-br 5086  df-opab 5148  df-mpt 5167  df-id 5526  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-iota 6454  df-fun 6500  df-fn 6501  df-f 6502  df-f1 6503  df-fo 6504  df-f1o 6505  df-fv 6506

This theorem is referenced by:  mptcnfimad  7939  fidmfisupp  9285  fdmfisuppfi  9287  fsuppco2  9316  fsuppcor  9317  ixpiunwdom  9505  cnfcom3clem  9626  fin23lem32  10266  hasheqf1od  14315  hashf1lem1  14417  fz1isolem  14423  ramval  16979  imasval  17475  imasle  17487  pwsco1mhm  18800  efgtf  19697  gsumval3a  19878  gsumval3lem1  19880  gsumval3lem2  19881  gsumval3  19882  gsumzres  19884  gsumzf1o  19887  gsumzaddlem  19896  gsumzadd  19897  gsumzmhm  19912  gsumzoppg  19919  gsumpt  19937  gsum2dlem2  19946  prdslmodd  20964  dsmmsubg  21723  dsmmlss  21724  islindf2  21794  f1lindf  21802  islindf4  21818  gsumply1subr  22197  txcn  23591  prdstps  23594  qtopval2  23661  fmval  23908  tsmsres  24109  tsmsadd  24112  jensen  26952  fisuppov1  32756  pwrssmgc  33060  gsumpart  33124  gsumwrd2dccat  33139  ply1degltdimlem  33766  ofcfval4  34249  omsfval  34438  omssubadd  34444  carsgval  34447  sseqval  34532  hgt750lemg  34798  filnetlem4  36563  bj-finsumval0  37599  isrngod  38219  isgrpda  38276  iscringd  38319  sticksstones8  42592  limsupre  46069  limsupval3  46120  limsuppnfdlem  46129  limsupvaluz  46136  limsuppnflem  46138  limsupre2lem  46152  climuzlem  46171  climisp  46174  climxrrelem  46177  climxrre  46178  liminfval5  46193  limsupgtlem  46205  liminfvalxr  46211  liminflelimsupuz  46213  liminfgelimsupuz  46216  liminflimsupclim  46235  liminflbuz2  46243  xlimclim2lem  46267  climxlim2  46274  fourierdlem71  46605  fourierdlem80  46614  sge0val  46794  sge0f1o  46810  isomennd  46959  nsssmfmbflem  47206  isuspgrim  48372  isubgr3stgrlem3  48444  isubgr3stgrlem5  48446  clnbgr3stgrgrlim  48495  itcovalendof  49145  thinccisod  49929