Theorem mptexd 7201

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

Syntax hints:   → wi 4   ∈ wcel 2109  Vcvv 3450   ↦ cmpt 5191

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 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-rep 5237  ax-sep 5254  ax-nul 5264  ax-pr 5390

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-ral 3046  df-rex 3055  df-reu 3357  df-rab 3409  df-v 3452  df-sbc 3757  df-csb 3866  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-iun 4960  df-br 5111  df-opab 5173  df-mpt 5192  df-id 5536  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-res 5653  df-ima 5654  df-iota 6467  df-fun 6516  df-fn 6517  df-f 6518  df-f1 6519  df-fo 6520  df-f1o 6521  df-fv 6522

This theorem is referenced by:  mptsuppdifd  8168  mpocurryvald  8252  fsetfocdm  8837  fsuppssov1  9342  fsuppmptif  9357  sniffsupp  9358  cantnfrescl  9636  cantnflem1  9649  infxpenc2lem2  9980  ac5num  9996  ac6num  10439  negfi  12139  seqof2  14032  ramcl  17007  prdsplusgval  17443  prdsmulrval  17445  prdsvscaval  17449  galactghm  19341  gsum2dlem2  19908  gsum2d  19909  dprdfinv  19958  dprdfadd  19959  dmdprdsplitlem  19976  dpjfval  19994  dpjidcl  19997  mptscmfsupp0  20840  frlmgsum  21688  frlmphllem  21696  psrass1lem  21848  psrridm  21879  psrcom  21884  mvrfval  21897  mplcoe5  21954  mplbas2  21956  evlslem6  21995  selvffval  22027  psdffval  22051  psdfval  22052  psdmplcl  22056  psdmul  22060  evls1sca  22217  evls1fpws  22263  matgsum  22331  mvmulval  22437  mavmul0g  22447  marepvval0  22460  ptcnplem  23515  xkocnv  23708  ptcmplem3  23948  prdsdsf  24262  ressprdsds  24266  prdsxmslem2  24424  rrx0  25304  tdeglem4  25972  pserulm  26338  efsubm  26467  addsuniflem  27915  suppovss  32611  fisuppov1  32613  mptiffisupp  32623  fsuppcurry1  32655  fsuppcurry2  32656  gsummptres2  33000  gsumfs2d  33002  tocycval  33072  rmfsupp2  33196  elrgspnlem2  33201  elrsp  33350  qusrn  33387  elrspunidl  33406  elrspunsn  33407  drgextgsum  33597  ply1degltdimlem  33625  fedgmullem2  33633  evls1fldgencl  33672  fldextrspunlsplem  33675  fldextrspunlsp  33676  minplyval  33702  ofcfval  34095  lpadval  34674  bj-imdirvallem  37175  hashscontpow  42117  aks6d1c2  42125  sticksstones4  42144  sticksstones11  42151  sticksstones12a  42152  sticksstones12  42153  sticksstones17  42158  sticksstones18  42159  sticksstones19  42160  sticksstones20  42161  aks6d1c6lem2  42166  aks6d1c6lem3  42167  aks6d1c7lem2  42176  aks5lem2  42182  evlsvvvallem  42556  evlsvvval  42558  selvvvval  42580  evlselv  42582  mhphf  42592  rfovfvd  43998  fsovfvd  44006  dssmapf1od  44017  choicefi  45201  axccdom  45223  climeldmeqmpt  45673  climfveqmpt  45676  climfveqmpt3  45687  climeldmeqmpt3  45694  climfveqmpt2  45698  climeldmeqmpt2  45700  climeqmpt  45702  limsupresicompt  45761  liminfresicompt  45785  liminfvalxr  45788  liminflbuz2  45820  iccvonmbllem  46683  vonioolem1  46685  vonioolem2  46686  vonicclem1  46688  vonicclem2  46689  smflimmpt  46815  smflimsuplem6  46830  cfsetsnfsetfv  47062  cfsetsnfsetf  47063  fundcmpsurbijinjpreimafv  47412  prproropen  47513  isubgr3stgr  47978  uspgrbispr  48143  1arymaptfv  48633  1arymaptfo  48636  fuco22  49332