Theorem mptexd 7109

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

Syntax hints:   → wi 4   ∈ wcel 2107  Vcvv 3433   ↦ cmpt 5158

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2710  ax-rep 5210  ax-sep 5224  ax-nul 5231  ax-pr 5353

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-nfc 2890  df-ne 2945  df-ral 3070  df-rex 3071  df-reu 3073  df-rab 3074  df-v 3435  df-sbc 3718  df-csb 3834  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-nul 4258  df-if 4461  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4841  df-iun 4927  df-br 5076  df-opab 5138  df-mpt 5159  df-id 5490  df-xp 5596  df-rel 5597  df-cnv 5598  df-co 5599  df-dm 5600  df-rn 5601  df-res 5602  df-ima 5603  df-iota 6395  df-fun 6439  df-fn 6440  df-f 6441  df-f1 6442  df-fo 6443  df-f1o 6444  df-fv 6445

This theorem is referenced by:  mptsuppdifd  8011  mpocurryvald  8095  fsetfocdm  8658  fsuppmptif  9167  sniffsupp  9168  cantnfrescl  9443  cantnflem1  9456  infxpenc2lem2  9785  ac5num  9801  ac6num  10244  negfi  11933  seqof2  13790  ramcl  16739  prdsplusgval  17193  prdsmulrval  17195  prdsvscaval  17199  galactghm  19021  gsum2dlem2  19581  gsum2d  19582  dprdfinv  19631  dprdfadd  19632  dmdprdsplitlem  19649  dpjfval  19667  dpjidcl  19670  mptscmfsupp0  20197  frlmgsum  20988  frlmphllem  20996  psrass1lemOLD  21152  psrass1lem  21155  psrridm  21182  psrcom  21187  mvrfval  21198  mplcoe5  21250  mplbas2  21252  evlslem6  21300  selvffval  21335  evls1sca  21498  matgsum  21595  mvmulval  21701  mavmul0g  21711  marepvval0  21724  ptcnplem  22781  xkocnv  22974  ptcmplem3  23214  prdsdsf  23529  ressprdsds  23533  prdsxmslem2  23694  rrx0  24570  tdeglem4  25233  tdeglem4OLD  25234  pserulm  25590  efsubm  25716  suppovss  31026  fsuppcurry1  31069  fsuppcurry2  31070  gsummptres2  31322  tocycval  31384  rmfsupp2  31501  elrsp  31578  elrspunidl  31615  drgextgsum  31691  fedgmullem2  31720  ofcfval  32075  lpadval  32665  bj-imdirvallem  35360  sticksstones4  40112  sticksstones11  40119  sticksstones12a  40120  sticksstones12  40121  sticksstones17  40126  sticksstones18  40127  sticksstones19  40128  sticksstones20  40129  evlsbagval  40282  mhphf  40292  rfovfvd  41617  fsovfvd  41625  dssmapf1od  41636  choicefi  42747  axccdom  42769  climeldmeqmpt  43216  climfveqmpt  43219  climfveqmpt3  43230  climeldmeqmpt3  43237  climfveqmpt2  43241  climeldmeqmpt2  43243  climeqmpt  43245  limsupresicompt  43304  liminfresicompt  43328  liminfvalxr  43331  liminflbuz2  43363  iccvonmbllem  44223  vonioolem1  44225  vonioolem2  44226  vonicclem1  44228  vonicclem2  44229  smflimmpt  44354  smflimsuplem6  44369  cfsetsnfsetfv  44562  cfsetsnfsetf  44563  fundcmpsurbijinjpreimafv  44870  prproropen  44971  uspgrbispr  45324  1arymaptfv  45997  1arymaptfo  46000