Theorem fexd 7171

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

Syntax hints:   → wi 4   ∈ wcel 2119  Vcvv 3431  ⟶wf 6481

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711  ax-rep 5199  ax-sep 5218  ax-nul 5228  ax-pr 5362

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2718  df-cleq 2731  df-clel 2814  df-nfc 2888  df-ne 2935  df-ral 3054  df-rex 3064  df-reu 3345  df-rab 3392  df-v 3433  df-sbc 3724  df-csb 3832  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4262  df-if 4455  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-iun 4923  df-br 5073  df-opab 5135  df-mpt 5154  df-id 5513  df-xp 5624  df-rel 5625  df-cnv 5626  df-co 5627  df-dm 5628  df-rn 5629  df-res 5630  df-ima 5631  df-iota 6441  df-fun 6487  df-fn 6488  df-f 6489  df-f1 6490  df-fo 6491  df-f1o 6492  df-fv 6493

This theorem is referenced by:  mptcnfimad  7928  fidmfisupp  9275  fdmfisuppfi  9277  fsuppco2  9306  fsuppcor  9307  ixpiunwdom  9495  cnfcom3clem  9617  fin23lem32  10257  hasheqf1od  14306  hashf1lem1  14408  fz1isolem  14414  ramval  16970  imasval  17466  imasle  17478  pwsco1mhm  18791  efgtf  19688  gsumval3a  19869  gsumval3lem1  19871  gsumval3lem2  19872  gsumval3  19873  gsumzres  19875  gsumzf1o  19878  gsumzaddlem  19887  gsumzadd  19888  gsumzmhm  19903  gsumzoppg  19910  gsumpt  19928  gsum2dlem2  19937  prdslmodd  20959  dsmmsubg  21718  dsmmlss  21719  islindf2  21789  f1lindf  21797  islindf4  21813  gsumply1subr  22218  txcn  23609  prdstps  23612  qtopval2  23679  fmval  23926  tsmsres  24127  tsmsadd  24130  jensen  26970  fisuppov1  32775  pwrssmgc  33079  gsumpart  33144  gsumwrd2dccat  33159  ply1degltdimlem  33806  ofcfval4  34289  omsfval  34478  omssubadd  34484  carsgval  34487  sseqval  34572  hgt750lemg  34838  filnetlem4  36609  bj-finsumval0  37645  isrngod  38265  isgrpda  38322  iscringd  38365  sticksstones8  42638  limsupre  46084  limsupval3  46135  limsuppnfdlem  46144  limsupvaluz  46151  limsuppnflem  46153  limsupre2lem  46167  climuzlem  46186  climisp  46189  climxrrelem  46192  climxrre  46193  liminfval5  46208  limsupgtlem  46220  liminfvalxr  46226  liminflelimsupuz  46228  liminfgelimsupuz  46231  liminflimsupclim  46250  liminflbuz2  46258  xlimclim2lem  46282  climxlim2  46289  fourierdlem71  46620  fourierdlem80  46629  sge0val  46809  sge0f1o  46825  isomennd  46974  nsssmfmbflem  47221  isuspgrim  48387  isubgr3stgrlem3  48459  isubgr3stgrlem5  48461  clnbgr3stgrgrlim  48510  itcovalendof  49160  thinccisod  49944