Theorem fexd 7231

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

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

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 2733  ax-rep 5232  ax-sep 5249  ax-nul 5260  ax-pr 5391

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 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3078  df-rex 3088  df-reu 3367  df-rab 3414  df-v 3453  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 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545

This theorem is used by:  mptcnfimad  7996  fidmfisupp  9357  fdmfisuppfi  9359  fsuppco2  9388  fsuppcor  9389  ixpiunwdom  9577  cnfcom3clem  9699  fin23lem32  10415  hasheqf1od  14490  hashf1lem1  14593  fz1isolem  14599  ramval  17179  imasval  17676  imasle  17688  pwsco1mhm  19021  efgtf  19929  gsumval3a  20110  gsumval3lem1  20112  gsumval3lem2  20113  gsumval3  20114  gsumzres  20116  gsumzf1o  20119  gsumzaddlem  20128  gsumzadd  20129  gsumzmhm  20144  gsumzoppg  20151  gsumpt  20169  gsum2dlem2  20178  prdslmodd  21237  dsmmsubg  22042  dsmmlss  22043  islindf2  22113  f1lindf  22121  islindf4  22137  gsumply1subr  22544  txcn  23938  prdstps  23941  qtopval2  24008  fmval  24255  tsmsres  24456  tsmsadd  24459  jensen  27309  fisuppov1  33269  pwrssmgc  33554  gsumpart  33617  gsumwrd2dccat  33632  ply1degltdimlem  34247  ofcfval4  34730  omsfval  34919  omssubadd  34925  carsgval  34928  sseqval  35013  hgt750lemg  35276  filnetlem4  37149  bj-finsumval0  38186  isrngod  38812  isgrpda  38869  iscringd  38912  sticksstones8  43183  limsupre  46620  limsupval3  46671  limsuppnfdlem  46680  limsupvaluz  46687  limsuppnflem  46689  limsupre2lem  46703  climuzlem  46722  climisp  46725  climxrrelem  46728  climxrre  46729  liminfval5  46744  limsupgtlem  46756  liminfvalxr  46762  liminflelimsupuz  46764  liminfgelimsupuz  46767  liminflimsupclim  46786  liminflbuz2  46794  xlimclim2lem  46818  climxlim2  46825  fourierdlem71  47156  fourierdlem80  47165  sge0val  47345  sge0f1o  47361  isomennd  47510  nsssmfmbflem  47757  isuspgrim  48963  isubgr3stgrlem3  49035  isubgr3stgrlem5  49037  clnbgr3stgrgrlim  49086  itcovalendof  49750  thinccisod  50531