Theorem fexd 7226

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 7225	. 2 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐴 ∈ 𝐶) → 𝐹 ∈ V)
4	1, 2, 3	syl2anc 596	1 ⊢ (𝜑 → 𝐹 ∈ V)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  Vcvv 3450  ⟶wf 6529

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-rep 5232  ax-sep 5251  ax-nul 5263  ax-pr 5398

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-iun 4953  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5550  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-iota 6489  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541

This theorem is used by:  mptcnfimad  7983  fidmfisupp  9342  fdmfisuppfi  9344  fsuppco2  9373  fsuppcor  9374  ixpiunwdom  9562  cnfcom3clem  9684  fin23lem32  10346  hasheqf1od  14417  hashf1lem1  14520  fz1isolem  14526  ramval  17100  imasval  17597  imasle  17609  pwsco1mhm  18941  efgtf  19849  gsumval3a  20030  gsumval3lem1  20032  gsumval3lem2  20033  gsumval3  20034  gsumzres  20036  gsumzf1o  20039  gsumzaddlem  20048  gsumzadd  20049  gsumzmhm  20064  gsumzoppg  20071  gsumpt  20089  gsum2dlem2  20098  prdslmodd  21153  dsmmsubg  21956  dsmmlss  21957  islindf2  22027  f1lindf  22035  islindf4  22051  gsumply1subr  22458  txcn  23852  prdstps  23855  qtopval2  23922  fmval  24169  tsmsres  24370  tsmsadd  24373  jensen  27225  fisuppov1  33155  pwrssmgc  33440  gsumpart  33503  gsumwrd2dccat  33518  ply1degltdimlem  34132  ofcfval4  34615  omsfval  34805  omssubadd  34811  carsgval  34814  sseqval  34899  hgt750lemg  35162  filnetlem4  37000  bj-finsumval0  38037  isrngod  38648  isgrpda  38705  iscringd  38748  sticksstones8  43019  limsupre  46469  limsupval3  46520  limsuppnfdlem  46529  limsupvaluz  46536  limsuppnflem  46538  limsupre2lem  46552  climuzlem  46571  climisp  46574  climxrrelem  46577  climxrre  46578  liminfval5  46593  limsupgtlem  46605  liminfvalxr  46611  liminflelimsupuz  46613  liminfgelimsupuz  46616  liminflimsupclim  46635  liminflbuz2  46643  xlimclim2lem  46667  climxlim2  46674  fourierdlem71  47005  fourierdlem80  47014  sge0val  47194  sge0f1o  47210  isomennd  47359  nsssmfmbflem  47606  isuspgrim  48812  isubgr3stgrlem3  48884  isubgr3stgrlem5  48886  clnbgr3stgrgrlim  48935  itcovalendof  49599  thinccisod  50380