Theorem mptexd 7222

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

Syntax hints:   → wi 4   ∈ wcel 2106  Vcvv 3474   ↦ cmpt 5230

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-rep 5284  ax-sep 5298  ax-nul 5305  ax-pr 5426

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-ral 3062  df-rex 3071  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-iun 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5573  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548

This theorem is referenced by:  mptsuppdifd  8167  mpocurryvald  8251  fsetfocdm  8851  fsuppmptif  9390  sniffsupp  9391  cantnfrescl  9667  cantnflem1  9680  infxpenc2lem2  10011  ac5num  10027  ac6num  10470  negfi  12159  seqof2  14022  ramcl  16958  prdsplusgval  17415  prdsmulrval  17417  prdsvscaval  17421  galactghm  19266  gsum2dlem2  19833  gsum2d  19834  dprdfinv  19883  dprdfadd  19884  dmdprdsplitlem  19901  dpjfval  19919  dpjidcl  19922  mptscmfsupp0  20529  frlmgsum  21318  frlmphllem  21326  psrass1lemOLD  21484  psrass1lem  21487  psrridm  21515  psrcom  21520  mvrfval  21531  mplcoe5  21586  mplbas2  21588  evlslem6  21635  selvffval  21670  evls1sca  21833  matgsum  21930  mvmulval  22036  mavmul0g  22046  marepvval0  22059  ptcnplem  23116  xkocnv  23309  ptcmplem3  23549  prdsdsf  23864  ressprdsds  23868  prdsxmslem2  24029  rrx0  24905  tdeglem4  25568  tdeglem4OLD  25569  pserulm  25925  efsubm  26051  addsuniflem  27473  suppovss  31893  mptiffisupp  31902  fsuppcurry1  31937  fsuppcurry2  31938  gsummptres2  32192  tocycval  32254  rmfsupp2  32375  elrsp  32474  qusrn  32508  elrspunidl  32534  elrspunsn  32535  evls1fpws  32634  drgextgsum  32670  ply1degltdimlem  32695  fedgmullem2  32703  minplyval  32754  ofcfval  33084  lpadval  33676  bj-imdirvallem  36049  sticksstones4  40953  sticksstones11  40960  sticksstones12a  40961  sticksstones12  40962  sticksstones17  40967  sticksstones18  40968  sticksstones19  40969  sticksstones20  40970  evlsvvvallem  41130  evlsvvval  41132  selvvvval  41154  evlselv  41156  mhphf  41166  rfovfvd  42738  fsovfvd  42746  dssmapf1od  42757  choicefi  43884  axccdom  43906  climeldmeqmpt  44370  climfveqmpt  44373  climfveqmpt3  44384  climeldmeqmpt3  44391  climfveqmpt2  44395  climeldmeqmpt2  44397  climeqmpt  44399  limsupresicompt  44458  liminfresicompt  44482  liminfvalxr  44485  liminflbuz2  44517  iccvonmbllem  45380  vonioolem1  45382  vonioolem2  45383  vonicclem1  45385  vonicclem2  45386  smflimmpt  45512  smflimsuplem6  45527  cfsetsnfsetfv  45753  cfsetsnfsetf  45754  fundcmpsurbijinjpreimafv  46061  prproropen  46162  uspgrbispr  46515  1arymaptfv  47279  1arymaptfo  47282