Theorem mptexd 7198

Description: If the domain of a function given by maps-to notation is a set, the function is a set. Deduction version of mptexg 7195. (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 7195	. 2 ⊢ (𝐴 ∈ 𝑉 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ V)
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ V)

Syntax hints:   → wi 4   ∈ wcel 2109  Vcvv 3447   ↦ cmpt 5188

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 5234  ax-sep 5251  ax-nul 5261  ax-pr 5387

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 3355  df-rab 3406  df-v 3449  df-sbc 3754  df-csb 3863  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-iun 4957  df-br 5108  df-opab 5170  df-mpt 5189  df-id 5533  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-iota 6464  df-fun 6513  df-fn 6514  df-f 6515  df-f1 6516  df-fo 6517  df-f1o 6518  df-fv 6519

This theorem is referenced by:  mptsuppdifd  8165  mpocurryvald  8249  fsetfocdm  8834  fsuppssov1  9335  fsuppmptif  9350  sniffsupp  9351  cantnfrescl  9629  cantnflem1  9642  infxpenc2lem2  9973  ac5num  9989  ac6num  10432  negfi  12132  seqof2  14025  ramcl  17000  prdsplusgval  17436  prdsmulrval  17438  prdsvscaval  17442  galactghm  19334  gsum2dlem2  19901  gsum2d  19902  dprdfinv  19951  dprdfadd  19952  dmdprdsplitlem  19969  dpjfval  19987  dpjidcl  19990  mptscmfsupp0  20833  frlmgsum  21681  frlmphllem  21689  psrass1lem  21841  psrridm  21872  psrcom  21877  mvrfval  21890  mplcoe5  21947  mplbas2  21949  evlslem6  21988  selvffval  22020  psdffval  22044  psdfval  22045  psdmplcl  22049  psdmul  22053  evls1sca  22210  evls1fpws  22256  matgsum  22324  mvmulval  22430  mavmul0g  22440  marepvval0  22453  ptcnplem  23508  xkocnv  23701  ptcmplem3  23941  prdsdsf  24255  ressprdsds  24259  prdsxmslem2  24417  rrx0  25297  tdeglem4  25965  pserulm  26331  efsubm  26460  addsuniflem  27908  suppovss  32604  fisuppov1  32606  mptiffisupp  32616  fsuppcurry1  32648  fsuppcurry2  32649  gsummptres2  32993  gsumfs2d  32995  tocycval  33065  rmfsupp2  33189  elrgspnlem2  33194  elrsp  33343  qusrn  33380  elrspunidl  33399  elrspunsn  33400  drgextgsum  33590  ply1degltdimlem  33618  fedgmullem2  33626  evls1fldgencl  33665  fldextrspunlsplem  33668  fldextrspunlsp  33669  minplyval  33695  ofcfval  34088  lpadval  34667  bj-imdirvallem  37168  hashscontpow  42110  aks6d1c2  42118  sticksstones4  42137  sticksstones11  42144  sticksstones12a  42145  sticksstones12  42146  sticksstones17  42151  sticksstones18  42152  sticksstones19  42153  sticksstones20  42154  aks6d1c6lem2  42159  aks6d1c6lem3  42160  aks6d1c7lem2  42169  aks5lem2  42175  evlsvvvallem  42549  evlsvvval  42551  selvvvval  42573  evlselv  42575  mhphf  42585  rfovfvd  43991  fsovfvd  43999  dssmapf1od  44010  choicefi  45194  axccdom  45216  climeldmeqmpt  45666  climfveqmpt  45669  climfveqmpt3  45680  climeldmeqmpt3  45687  climfveqmpt2  45691  climeldmeqmpt2  45693  climeqmpt  45695  limsupresicompt  45754  liminfresicompt  45778  liminfvalxr  45781  liminflbuz2  45813  iccvonmbllem  46676  vonioolem1  46678  vonioolem2  46679  vonicclem1  46681  vonicclem2  46682  smflimmpt  46808  smflimsuplem6  46823  cfsetsnfsetfv  47058  cfsetsnfsetf  47059  fundcmpsurbijinjpreimafv  47408  prproropen  47509  isubgr3stgr  47974  uspgrbispr  48139  1arymaptfv  48629  1arymaptfo  48632  fuco22  49328