Theorem fexd 7112

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

Syntax hints:   → wi 4   ∈ wcel 2107  Vcvv 3433  ⟶wf 6433

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2710  ax-rep 5210  ax-sep 5224  ax-nul 5231  ax-pr 5353

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-nfc 2890  df-ne 2945  df-ral 3070  df-rex 3071  df-reu 3073  df-rab 3074  df-v 3435  df-sbc 3718  df-csb 3834  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-nul 4258  df-if 4461  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4841  df-iun 4927  df-br 5076  df-opab 5138  df-mpt 5159  df-id 5490  df-xp 5596  df-rel 5597  df-cnv 5598  df-co 5599  df-dm 5600  df-rn 5601  df-res 5602  df-ima 5603  df-iota 6395  df-fun 6439  df-fn 6440  df-f 6441  df-f1 6442  df-fo 6443  df-f1o 6444  df-fv 6445

This theorem is referenced by:  fdmfisuppfi  9146  fsuppco2  9171  fsuppcor  9172  ixpiunwdom  9358  cnfcom3clem  9472  fin23lem32  10109  hasheqf1od  14077  hashf1lem1  14177  hashf1lem1OLD  14178  fz1isolem  14184  ramval  16718  imasval  17231  imasle  17243  pwsco1mhm  18479  efgtf  19337  gsumval3a  19513  gsumval3lem1  19515  gsumval3lem2  19516  gsumval3  19517  gsumzres  19519  gsumzf1o  19522  gsumzaddlem  19531  gsumzadd  19532  gsumzmhm  19547  gsumzoppg  19554  gsumpt  19572  gsum2dlem2  19581  prdslmodd  20240  dsmmsubg  20959  dsmmlss  20960  islindf2  21030  f1lindf  21038  islindf4  21054  gsumply1subr  21414  txcn  22786  prdstps  22789  qtopval2  22856  fmval  23103  tsmsres  23304  tsmsadd  23307  jensen  26147  pwrssmgc  31287  gsumpart  31324  ofcfval4  32082  omsfval  32270  omssubadd  32276  carsgval  32279  sseqval  32364  hgt750lemg  32643  filnetlem4  34579  bj-finsumval0  35465  isrngod  36065  isgrpda  36122  iscringd  36165  sticksstones8  40116  fidmfisupp  42746  limsupre  43189  limsupval3  43240  limsuppnfdlem  43249  limsupvaluz  43256  limsuppnflem  43258  limsupre2lem  43272  climuzlem  43291  climisp  43294  climxrrelem  43297  climxrre  43298  liminfval5  43313  limsupgtlem  43325  liminfvalxr  43331  liminflelimsupuz  43333  liminfgelimsupuz  43336  liminflimsupclim  43355  liminflbuz2  43363  xlimclim2lem  43387  climxlim2  43394  fourierdlem71  43725  fourierdlem80  43734  sge0val  43911  sge0f1o  43927  isomennd  44076  nsssmfmbflem  44323  itcovalendof  46026