Theorem mptexd 7243

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

Syntax hints:   → wi 4   ∈ wcel 2105  Vcvv 3477   ↦ cmpt 5230

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-rep 5284  ax-sep 5301  ax-nul 5311  ax-pr 5437

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-ral 3059  df-rex 3068  df-reu 3378  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-iun 4997  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5582  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569  df-fv 6570

This theorem is referenced by:  mptsuppdifd  8209  mpocurryvald  8293  fsetfocdm  8899  fsuppssov1  9421  fsuppmptif  9436  sniffsupp  9437  cantnfrescl  9713  cantnflem1  9726  infxpenc2lem2  10057  ac5num  10073  ac6num  10516  negfi  12214  seqof2  14097  ramcl  17062  prdsplusgval  17519  prdsmulrval  17521  prdsvscaval  17525  galactghm  19436  gsum2dlem2  20003  gsum2d  20004  dprdfinv  20053  dprdfadd  20054  dmdprdsplitlem  20071  dpjfval  20089  dpjidcl  20092  mptscmfsupp0  20941  frlmgsum  21809  frlmphllem  21817  psrass1lem  21969  psrridm  22000  psrcom  22005  mvrfval  22018  mplcoe5  22075  mplbas2  22077  evlslem6  22122  selvffval  22154  psdffval  22178  psdfval  22179  psdmplcl  22183  psdmul  22187  evls1sca  22342  evls1fpws  22388  matgsum  22458  mvmulval  22564  mavmul0g  22574  marepvval0  22587  ptcnplem  23644  xkocnv  23837  ptcmplem3  24077  prdsdsf  24392  ressprdsds  24396  prdsxmslem2  24557  rrx0  25444  tdeglem4  26113  pserulm  26479  efsubm  26607  addsuniflem  28048  suppovss  32695  fisuppov1  32697  mptiffisupp  32707  fsuppcurry1  32742  fsuppcurry2  32743  gsummptres2  33038  gsumfs2d  33040  tocycval  33110  rmfsupp2  33227  elrgspnlem2  33232  elrsp  33379  qusrn  33416  elrspunidl  33435  elrspunsn  33436  drgextgsum  33623  ply1degltdimlem  33649  fedgmullem2  33657  evls1fldgencl  33694  minplyval  33712  ofcfval  34078  lpadval  34669  bj-imdirvallem  37162  hashscontpow  42103  aks6d1c2  42111  sticksstones4  42130  sticksstones11  42137  sticksstones12a  42138  sticksstones12  42139  sticksstones17  42144  sticksstones18  42145  sticksstones19  42146  sticksstones20  42147  aks6d1c6lem2  42152  aks6d1c6lem3  42153  aks6d1c7lem2  42162  aks5lem2  42168  evlsvvvallem  42547  evlsvvval  42549  selvvvval  42571  evlselv  42573  mhphf  42583  rfovfvd  43991  fsovfvd  43999  dssmapf1od  44010  choicefi  45142  axccdom  45164  climeldmeqmpt  45623  climfveqmpt  45626  climfveqmpt3  45637  climeldmeqmpt3  45644  climfveqmpt2  45648  climeldmeqmpt2  45650  climeqmpt  45652  limsupresicompt  45711  liminfresicompt  45735  liminfvalxr  45738  liminflbuz2  45770  iccvonmbllem  46633  vonioolem1  46635  vonioolem2  46636  vonicclem1  46638  vonicclem2  46639  smflimmpt  46765  smflimsuplem6  46780  cfsetsnfsetfv  47006  cfsetsnfsetf  47007  fundcmpsurbijinjpreimafv  47331  prproropen  47432  isubgr3stgr  47877  uspgrbispr  47994  1arymaptfv  48489  1arymaptfo  48492