Theorem mptexd 7212

Description: If the domain of a function given by maps-to notation is a set, the function is a set. Deduction version of mptexg 7209. (Contributed by Glauco Siliprandi, 24-Dec-2020.)

Hypothesis

Ref	Expression
mptexd.1	⊢ (𝜑 → 𝐴 ∈ 𝑉)

Assertion

Ref	Expression
mptexd	⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ V)

Distinct variable group:   𝑥,𝐴

Allowed substitution hints:   𝜑(𝑥)   𝐵(𝑥)   𝑉(𝑥)

Proof of Theorem mptexd

Step	Hyp	Ref	Expression
1		mptexd.1	. 2 ⊢ (𝜑 → 𝐴 ∈ 𝑉)
2		mptexg 7209	. 2 ⊢ (𝐴 ∈ 𝑉 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ V)
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ V)

Syntax hints:   → wi 4   ∈ wcel 2107  Vcvv 3457   ↦ cmpt 5198

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2706  ax-rep 5246  ax-sep 5263  ax-nul 5273  ax-pr 5399

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2808  df-nfc 2884  df-ne 2932  df-ral 3051  df-rex 3060  df-reu 3358  df-rab 3414  df-v 3459  df-sbc 3764  df-csb 3873  df-dif 3927  df-un 3929  df-in 3931  df-ss 3941  df-nul 4307  df-if 4499  df-sn 4600  df-pr 4602  df-op 4606  df-uni 4881  df-iun 4966  df-br 5117  df-opab 5179  df-mpt 5199  df-id 5545  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-iota 6480  df-fun 6529  df-fn 6530  df-f 6531  df-f1 6532  df-fo 6533  df-f1o 6534  df-fv 6535

This theorem is referenced by:  mptsuppdifd  8179  mpocurryvald  8263  fsetfocdm  8869  fsuppssov1  9390  fsuppmptif  9405  sniffsupp  9406  cantnfrescl  9682  cantnflem1  9695  infxpenc2lem2  10026  ac5num  10042  ac6num  10485  negfi  12183  seqof2  14067  ramcl  17034  prdsplusgval  17472  prdsmulrval  17474  prdsvscaval  17478  galactghm  19370  gsum2dlem2  19937  gsum2d  19938  dprdfinv  19987  dprdfadd  19988  dmdprdsplitlem  20005  dpjfval  20023  dpjidcl  20026  mptscmfsupp0  20869  frlmgsum  21717  frlmphllem  21725  psrass1lem  21877  psrridm  21908  psrcom  21913  mvrfval  21926  mplcoe5  21983  mplbas2  21985  evlslem6  22024  selvffval  22056  psdffval  22080  psdfval  22081  psdmplcl  22085  psdmul  22089  evls1sca  22246  evls1fpws  22292  matgsum  22360  mvmulval  22466  mavmul0g  22476  marepvval0  22489  ptcnplem  23544  xkocnv  23737  ptcmplem3  23977  prdsdsf  24291  ressprdsds  24295  prdsxmslem2  24453  rrx0  25334  tdeglem4  26002  pserulm  26368  efsubm  26496  addsuniflem  27937  suppovss  32591  fisuppov1  32593  mptiffisupp  32603  fsuppcurry1  32637  fsuppcurry2  32638  gsummptres2  32965  gsumfs2d  32967  tocycval  33037  rmfsupp2  33151  elrgspnlem2  33156  elrsp  33305  qusrn  33342  elrspunidl  33361  elrspunsn  33362  drgextgsum  33550  ply1degltdimlem  33578  fedgmullem2  33586  evls1fldgencl  33627  fldextrspunlsplem  33630  fldextrspunlsp  33631  minplyval  33655  ofcfval  34037  lpadval  34629  bj-imdirvallem  37119  hashscontpow  42057  aks6d1c2  42065  sticksstones4  42084  sticksstones11  42091  sticksstones12a  42092  sticksstones12  42093  sticksstones17  42098  sticksstones18  42099  sticksstones19  42100  sticksstones20  42101  aks6d1c6lem2  42106  aks6d1c6lem3  42107  aks6d1c7lem2  42116  aks5lem2  42122  evlsvvvallem  42509  evlsvvval  42511  selvvvval  42533  evlselv  42535  mhphf  42545  rfovfvd  43951  fsovfvd  43959  dssmapf1od  43970  choicefi  45151  axccdom  45173  climeldmeqmpt  45627  climfveqmpt  45630  climfveqmpt3  45641  climeldmeqmpt3  45648  climfveqmpt2  45652  climeldmeqmpt2  45654  climeqmpt  45656  limsupresicompt  45715  liminfresicompt  45739  liminfvalxr  45742  liminflbuz2  45774  iccvonmbllem  46637  vonioolem1  46639  vonioolem2  46640  vonicclem1  46642  vonicclem2  46643  smflimmpt  46769  smflimsuplem6  46784  cfsetsnfsetfv  47014  cfsetsnfsetf  47015  fundcmpsurbijinjpreimafv  47339  prproropen  47440  isubgr3stgr  47887  uspgrbispr  48012  1arymaptfv  48506  1arymaptfo  48509  fuco22  49056