Theorem fexd 7264

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

Syntax hints:   → wi 4   ∈ wcel 2108  Vcvv 3488  ⟶wf 6569

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-rep 5303  ax-sep 5317  ax-nul 5324  ax-pr 5447

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ne 2947  df-ral 3068  df-rex 3077  df-reu 3389  df-rab 3444  df-v 3490  df-sbc 3805  df-csb 3922  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-iun 5017  df-br 5167  df-opab 5229  df-mpt 5250  df-id 5593  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713  df-iota 6525  df-fun 6575  df-fn 6576  df-f 6577  df-f1 6578  df-fo 6579  df-f1o 6580  df-fv 6581

This theorem is referenced by:  mptcnfimad  8027  fidmfisupp  9442  fdmfisuppfi  9443  fsuppco2  9472  fsuppcor  9473  ixpiunwdom  9659  cnfcom3clem  9774  fin23lem32  10413  hasheqf1od  14402  hashf1lem1  14504  fz1isolem  14510  ramval  17055  imasval  17571  imasle  17583  pwsco1mhm  18867  efgtf  19764  gsumval3a  19945  gsumval3lem1  19947  gsumval3lem2  19948  gsumval3  19949  gsumzres  19951  gsumzf1o  19954  gsumzaddlem  19963  gsumzadd  19964  gsumzmhm  19979  gsumzoppg  19986  gsumpt  20004  gsum2dlem2  20013  prdslmodd  20990  dsmmsubg  21786  dsmmlss  21787  islindf2  21857  f1lindf  21865  islindf4  21881  gsumply1subr  22256  txcn  23655  prdstps  23658  qtopval2  23725  fmval  23972  tsmsres  24173  tsmsadd  24176  jensen  27050  pwrssmgc  32973  gsumpart  33038  ply1degltdimlem  33635  ofcfval4  34069  omsfval  34259  omssubadd  34265  carsgval  34268  sseqval  34353  hgt750lemg  34631  filnetlem4  36347  bj-finsumval0  37251  isrngod  37858  isgrpda  37915  iscringd  37958  sticksstones8  42110  limsupre  45562  limsupval3  45613  limsuppnfdlem  45622  limsupvaluz  45629  limsuppnflem  45631  limsupre2lem  45645  climuzlem  45664  climisp  45667  climxrrelem  45670  climxrre  45671  liminfval5  45686  limsupgtlem  45698  liminfvalxr  45704  liminflelimsupuz  45706  liminfgelimsupuz  45709  liminflimsupclim  45728  liminflbuz2  45736  xlimclim2lem  45760  climxlim2  45767  fourierdlem71  46098  fourierdlem80  46107  sge0val  46287  sge0f1o  46303  isomennd  46452  nsssmfmbflem  46699  isuspgrim  47759  itcovalendof  48403