Theorem mptexd 7202

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

Syntax hints:   → wi 4   ∈ wcel 2141  Vcvv 3453   ↦ cmpt 5178

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-rep 5224  ax-sep 5243  ax-nul 5253  ax-pr 5387

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-nf 1803  df-sb 2090  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3076  df-rex 3086  df-reu 3367  df-rab 3414  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4284  df-if 4478  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4863  df-iun 4948  df-br 5098  df-opab 5160  df-mpt 5179  df-id 5538  df-xp 5649  df-rel 5650  df-cnv 5651  df-co 5652  df-dm 5653  df-rn 5654  df-res 5655  df-ima 5656  df-iota 6471  df-fun 6517  df-fn 6518  df-f 6519  df-f1 6520  df-fo 6521  df-f1o 6522  df-fv 6523

This theorem is referenced by:  mptsuppdifd  8159  mpocurryvald  8243  fsetfocdm  8835  fsuppssov1  9323  fsuppmptif  9338  sniffsupp  9339  cantnfrescl  9624  cantnflem1  9637  infxpenc2lem2  9969  ac5num  9985  ac6num  10429  negfi  12134  seqof2  14066  ramcl  17055  prdsplusgval  17492  prdsmulrval  17494  prdsvscaval  17498  galactghm  19434  gsum2dlem2  20001  gsum2d  20002  dprdfinv  20051  dprdfadd  20052  dmdprdsplitlem  20069  dpjfval  20087  dpjidcl  20090  mptscmfsupp0  20981  frlmgsum  21811  frlmphllem  21819  psrass1lem  21972  psrridm  22001  psrcom  22006  mvrfval  22019  mplcoe5  22080  mplbas2  22082  evlslem6  22121  evlsvvvallem  22131  evlsvvval  22133  selvffval  22158  selvvvval  22182  psdffval  22209  psdfval  22210  psdmplcl  22214  psdmul  22218  evls1sca  22373  evls1fpws  22419  matgsum  22484  mvmulval  22590  mavmul0g  22600  marepvval0  22613  ptcnplem  23668  xkocnv  23861  ptcmplem3  24101  prdsdsf  24414  ressprdsds  24418  prdsxmslem2  24576  rrx0  25446  tdeglem4  26107  pserulm  26472  efsubm  26603  addsuniflem  28081  suppovss  32843  fisuppov1  32845  mptiffisupp  32855  fsuppcurry1  32886  fsuppcurry2  32887  gsummptres2  33193  gsumfs2d  33201  tocycval  33248  rmfsupp2  33378  elrgspnlem2  33384  elrsp  33518  qusrn  33555  elrspunidl  33574  elrspunsn  33575  selvply1rhmlema  33775  selvply1rhmlemb  33776  selvply1rhmlem3  33779  selvply1rhmlem4  33780  selvply1rhmlem5  33781  extvval  33788  extvfv  33790  extvfvcl  33793  extvfvalf  33794  mplvrpmfgalem  33801  mplvrpmga  33802  mplvrpmmhm  33803  mplvrpmrhm  33804  psrmonmul2  33808  issply  33818  esplyfvaln  33831  drgextgsum  33852  ply1degltdimlem  33879  fedgmullem2  33887  evls1fldgencl  33927  fldextrspunlsplem  33930  fldextrspunlsp  33931  extdgfialglem1  33949  extdgfialglem2  33950  minplyval  33962  ofcfval  34355  lpadval  34933  bj-imdirvallem  37632  qmapex  38910  hashscontpow  42699  aks6d1c2  42707  sticksstones4  42726  sticksstones11  42733  sticksstones12a  42734  sticksstones12  42735  sticksstones17  42740  sticksstones18  42741  sticksstones19  42742  sticksstones20  42743  aks6d1c6lem2  42748  aks6d1c6lem3  42749  aks6d1c7lem2  42758  aks5lem2  42764  evlselv  43131  mhphf  43139  rfovfvd  44538  fsovfvd  44546  dssmapf1od  44557  choicefi  45737  axccdom  45758  climeldmeqmpt  46202  climfveqmpt  46205  climfveqmpt3  46216  climeldmeqmpt3  46223  climfveqmpt2  46227  climeldmeqmpt2  46229  climeqmpt  46231  limsupresicompt  46290  liminfresicompt  46314  liminfvalxr  46317  liminflbuz2  46349  iccvonmbllem  47212  vonioolem1  47214  vonioolem2  47215  vonicclem1  47217  vonicclem2  47218  smflimmpt  47344  smflimsuplem6  47359  cfsetsnfsetfv  47611  cfsetsnfsetf  47612  fundcmpsurbijinjpreimafv  47973  prproropen  48074  isubgr3stgr  48557  uspgrbispr  48733  1arymaptfv  49222  1arymaptfo  49225  fuco22  49920