Theorem mptexd 6997

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

Syntax hints:   → wi 4   ∈ wcel 2114  Vcvv 3398   ↦ cmpt 5110

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2162  ax-12 2179  ax-ext 2710  ax-rep 5154  ax-sep 5167  ax-nul 5174  ax-pr 5296

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2075  df-mo 2540  df-eu 2570  df-clab 2717  df-cleq 2730  df-clel 2811  df-nfc 2881  df-ne 2935  df-ral 3058  df-rex 3059  df-reu 3060  df-rab 3062  df-v 3400  df-sbc 3681  df-csb 3791  df-dif 3846  df-un 3848  df-in 3850  df-ss 3860  df-nul 4212  df-if 4415  df-sn 4517  df-pr 4519  df-op 4523  df-uni 4797  df-iun 4883  df-br 5031  df-opab 5093  df-mpt 5111  df-id 5429  df-xp 5531  df-rel 5532  df-cnv 5533  df-co 5534  df-dm 5535  df-rn 5536  df-res 5537  df-ima 5538  df-iota 6297  df-fun 6341  df-fn 6342  df-f 6343  df-f1 6344  df-fo 6345  df-f1o 6346  df-fv 6347

This theorem is referenced by:  mptsuppdifd  7881  mpocurryvald  7965  fsetfocdm  8471  fsuppmptif  8936  sniffsupp  8937  cantnfrescl  9212  cantnflem1  9225  infxpenc2lem2  9520  ac5num  9536  ac6num  9979  negfi  11667  seqof2  13520  ramcl  16465  prdsplusgval  16849  prdsmulrval  16851  prdsvscaval  16855  galactghm  18650  gsum2dlem2  19210  gsum2d  19211  dprdfinv  19260  dprdfadd  19261  dmdprdsplitlem  19278  dpjfval  19296  dpjidcl  19299  mptscmfsupp0  19818  frlmgsum  20588  frlmphllem  20596  psrass1lemOLD  20753  psrass1lem  20756  psrridm  20783  psrcom  20788  mvrfval  20799  mplcoe5  20851  mplbas2  20853  evlslem6  20895  selvffval  20930  evls1sca  21093  matgsum  21188  mvmulval  21294  mavmul0g  21304  marepvval0  21317  ptcnplem  22372  xkocnv  22565  ptcmplem3  22805  prdsdsf  23120  ressprdsds  23124  prdsxmslem2  23282  rrx0  24149  tdeglem4  24812  tdeglem4OLD  24813  pserulm  25169  efsubm  25295  suppovss  30592  fsuppcurry1  30635  fsuppcurry2  30636  gsummptres2  30890  tocycval  30952  rmfsupp2  31069  elrsp  31141  elrspunidl  31178  drgextgsum  31254  fedgmullem2  31283  ofcfval  31636  lpadval  32226  bj-imdirvallem  34992  sticksstones4  39731  evlsbagval  39874  mhphf  39884  rfovfvd  41176  fsovfvd  41184  dssmapf1od  41195  choicefi  42298  axccdom  42320  climeldmeqmpt  42771  climfveqmpt  42774  climfveqmpt3  42785  climeldmeqmpt3  42792  climfveqmpt2  42796  climeldmeqmpt2  42798  climeqmpt  42800  limsupresicompt  42859  liminfresicompt  42883  liminfvalxr  42886  liminflbuz2  42918  iccvonmbllem  43778  vonioolem1  43780  vonioolem2  43781  vonicclem1  43783  vonicclem2  43784  smflimmpt  43902  smflimsuplem6  43917  cfsetsnfsetfv  44109  cfsetsnfsetf  44110  fundcmpsurbijinjpreimafv  44413  prproropen  44514  uspgrbispr  44867  1arymaptfv  45540  1arymaptfo  45543