Theorem fexd 7183

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

Syntax hints:   → wi 4   ∈ wcel 2109  Vcvv 3444  ⟶wf 6495

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-rep 5229  ax-sep 5246  ax-nul 5256  ax-pr 5382

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-reu 3352  df-rab 3403  df-v 3446  df-sbc 3751  df-csb 3860  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-iun 4953  df-br 5103  df-opab 5165  df-mpt 5184  df-id 5526  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-iota 6452  df-fun 6501  df-fn 6502  df-f 6503  df-f1 6504  df-fo 6505  df-f1o 6506  df-fv 6507

This theorem is referenced by:  mptcnfimad  7944  fidmfisupp  9299  fdmfisuppfi  9301  fsuppco2  9330  fsuppcor  9331  ixpiunwdom  9519  cnfcom3clem  9634  fin23lem32  10273  hasheqf1od  14294  hashf1lem1  14396  fz1isolem  14402  ramval  16955  imasval  17450  imasle  17462  pwsco1mhm  18735  efgtf  19628  gsumval3a  19809  gsumval3lem1  19811  gsumval3lem2  19812  gsumval3  19813  gsumzres  19815  gsumzf1o  19818  gsumzaddlem  19827  gsumzadd  19828  gsumzmhm  19843  gsumzoppg  19850  gsumpt  19868  gsum2dlem2  19877  prdslmodd  20851  dsmmsubg  21628  dsmmlss  21629  islindf2  21699  f1lindf  21707  islindf4  21723  gsumply1subr  22094  txcn  23489  prdstps  23492  qtopval2  23559  fmval  23806  tsmsres  24007  tsmsadd  24010  jensen  26875  fisuppov1  32579  pwrssmgc  32899  gsumpart  32970  gsumwrd2dccat  32980  ply1degltdimlem  33591  ofcfval4  34068  omsfval  34258  omssubadd  34264  carsgval  34267  sseqval  34352  hgt750lemg  34618  filnetlem4  36342  bj-finsumval0  37246  isrngod  37865  isgrpda  37922  iscringd  37965  sticksstones8  42114  limsupre  45612  limsupval3  45663  limsuppnfdlem  45672  limsupvaluz  45679  limsuppnflem  45681  limsupre2lem  45695  climuzlem  45714  climisp  45717  climxrrelem  45720  climxrre  45721  liminfval5  45736  limsupgtlem  45748  liminfvalxr  45754  liminflelimsupuz  45756  liminfgelimsupuz  45759  liminflimsupclim  45778  liminflbuz2  45786  xlimclim2lem  45810  climxlim2  45817  fourierdlem71  46148  fourierdlem80  46157  sge0val  46337  sge0f1o  46353  isomennd  46502  nsssmfmbflem  46749  isuspgrim  47869  isubgr3stgrlem3  47940  isubgr3stgrlem5  47942  itcovalendof  48631  thinccisod  49416