Theorem fexd 7229

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146  Vcvv 3458  ⟶wf 6536

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 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2738  ax-rep 5241  ax-sep 5260  ax-nul 5272  ax-pr 5407

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 2570  df-eu 2600  df-clab 2745  df-cleq 2758  df-clel 2841  df-nfc 2915  df-ne 2962  df-ral 3083  df-rex 3093  df-reu 3373  df-rab 3420  df-v 3460  df-sbc 3748  df-csb 3857  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4290  df-if 4491  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4876  df-iun 4961  df-br 5113  df-opab 5177  df-mpt 5196  df-id 5559  df-xp 5670  df-rel 5671  df-cnv 5672  df-co 5673  df-dm 5674  df-rn 5675  df-res 5676  df-ima 5677  df-iota 6496  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548

This theorem is used by:  mptcnfimad  7985  fidmfisupp  9334  fdmfisuppfi  9336  fsuppco2  9365  fsuppcor  9366  ixpiunwdom  9554  cnfcom3clem  9676  fin23lem32  10338  hasheqf1od  14400  hashf1lem1  14503  fz1isolem  14509  ramval  17078  imasval  17575  imasle  17587  pwsco1mhm  18901  efgtf  19802  gsumval3a  19983  gsumval3lem1  19985  gsumval3lem2  19986  gsumval3  19987  gsumzres  19989  gsumzf1o  19992  gsumzaddlem  20001  gsumzadd  20002  gsumzmhm  20017  gsumzoppg  20024  gsumpt  20042  gsum2dlem2  20051  prdslmodd  21105  dsmmsubg  21908  dsmmlss  21909  islindf2  21979  f1lindf  21987  islindf4  22003  gsumply1subr  22408  txcn  23798  prdstps  23801  qtopval2  23868  fmval  24115  tsmsres  24316  tsmsadd  24319  jensen  27168  fisuppov1  33043  pwrssmgc  33333  gsumpart  33396  gsumwrd2dccat  33411  ply1degltdimlem  34025  ofcfval4  34508  omsfval  34697  omssubadd  34703  carsgval  34706  sseqval  34791  hgt750lemg  35054  filnetlem4  36924  bj-finsumval0  37961  isrngod  38581  isgrpda  38638  iscringd  38681  sticksstones8  42952  limsupre  46387  limsupval3  46438  limsuppnfdlem  46447  limsupvaluz  46454  limsuppnflem  46456  limsupre2lem  46470  climuzlem  46489  climisp  46492  climxrrelem  46495  climxrre  46496  liminfval5  46511  limsupgtlem  46523  liminfvalxr  46529  liminflelimsupuz  46531  liminfgelimsupuz  46534  liminflimsupclim  46553  liminflbuz2  46561  xlimclim2lem  46585  climxlim2  46592  fourierdlem71  46923  fourierdlem80  46932  sge0val  47112  sge0f1o  47128  isomennd  47277  nsssmfmbflem  47524  isuspgrim  48693  isubgr3stgrlem3  48765  isubgr3stgrlem5  48767  clnbgr3stgrgrlim  48816  itcovalendof  49481  thinccisod  50264