Theorem mptexd 7244

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

Syntax hints:   → wi 4   ∈ wcel 2108  Vcvv 3480   ↦ cmpt 5225

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-rep 5279  ax-sep 5296  ax-nul 5306  ax-pr 5432

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-ral 3062  df-rex 3071  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-iun 4993  df-br 5144  df-opab 5206  df-mpt 5226  df-id 5578  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569

This theorem is referenced by:  mptsuppdifd  8211  mpocurryvald  8295  fsetfocdm  8901  fsuppssov1  9424  fsuppmptif  9439  sniffsupp  9440  cantnfrescl  9716  cantnflem1  9729  infxpenc2lem2  10060  ac5num  10076  ac6num  10519  negfi  12217  seqof2  14101  ramcl  17067  prdsplusgval  17518  prdsmulrval  17520  prdsvscaval  17524  galactghm  19422  gsum2dlem2  19989  gsum2d  19990  dprdfinv  20039  dprdfadd  20040  dmdprdsplitlem  20057  dpjfval  20075  dpjidcl  20078  mptscmfsupp0  20925  frlmgsum  21792  frlmphllem  21800  psrass1lem  21952  psrridm  21983  psrcom  21988  mvrfval  22001  mplcoe5  22058  mplbas2  22060  evlslem6  22105  selvffval  22137  psdffval  22161  psdfval  22162  psdmplcl  22166  psdmul  22170  evls1sca  22327  evls1fpws  22373  matgsum  22443  mvmulval  22549  mavmul0g  22559  marepvval0  22572  ptcnplem  23629  xkocnv  23822  ptcmplem3  24062  prdsdsf  24377  ressprdsds  24381  prdsxmslem2  24542  rrx0  25431  tdeglem4  26099  pserulm  26465  efsubm  26593  addsuniflem  28034  suppovss  32690  fisuppov1  32692  mptiffisupp  32702  fsuppcurry1  32736  fsuppcurry2  32737  gsummptres2  33056  gsumfs2d  33058  tocycval  33128  rmfsupp2  33242  elrgspnlem2  33247  elrsp  33400  qusrn  33437  elrspunidl  33456  elrspunsn  33457  drgextgsum  33645  ply1degltdimlem  33673  fedgmullem2  33681  evls1fldgencl  33720  fldextrspunlsplem  33723  fldextrspunlsp  33724  minplyval  33748  ofcfval  34099  lpadval  34691  bj-imdirvallem  37181  hashscontpow  42123  aks6d1c2  42131  sticksstones4  42150  sticksstones11  42157  sticksstones12a  42158  sticksstones12  42159  sticksstones17  42164  sticksstones18  42165  sticksstones19  42166  sticksstones20  42167  aks6d1c6lem2  42172  aks6d1c6lem3  42173  aks6d1c7lem2  42182  aks5lem2  42188  evlsvvvallem  42571  evlsvvval  42573  selvvvval  42595  evlselv  42597  mhphf  42607  rfovfvd  44015  fsovfvd  44023  dssmapf1od  44034  choicefi  45205  axccdom  45227  climeldmeqmpt  45683  climfveqmpt  45686  climfveqmpt3  45697  climeldmeqmpt3  45704  climfveqmpt2  45708  climeldmeqmpt2  45710  climeqmpt  45712  limsupresicompt  45771  liminfresicompt  45795  liminfvalxr  45798  liminflbuz2  45830  iccvonmbllem  46693  vonioolem1  46695  vonioolem2  46696  vonicclem1  46698  vonicclem2  46699  smflimmpt  46825  smflimsuplem6  46840  cfsetsnfsetfv  47069  cfsetsnfsetf  47070  fundcmpsurbijinjpreimafv  47394  prproropen  47495  isubgr3stgr  47942  uspgrbispr  48067  1arymaptfv  48561  1arymaptfo  48564  fuco22  49034