Theorem mptexd 7179

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

Syntax hints:   → wi 4   ∈ wcel 2114  Vcvv 3429   ↦ cmpt 5166

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2708  ax-rep 5212  ax-sep 5231  ax-nul 5241  ax-pr 5375

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3062  df-reu 3343  df-rab 3390  df-v 3431  df-sbc 3729  df-csb 3838  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-iun 4935  df-br 5086  df-opab 5148  df-mpt 5167  df-id 5526  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-iota 6454  df-fun 6500  df-fn 6501  df-f 6502  df-f1 6503  df-fo 6504  df-f1o 6505  df-fv 6506

This theorem is referenced by:  mptsuppdifd  8136  mpocurryvald  8220  fsetfocdm  8808  fsuppssov1  9297  fsuppmptif  9312  sniffsupp  9313  cantnfrescl  9597  cantnflem1  9610  infxpenc2lem2  9942  ac5num  9958  ac6num  10401  negfi  12105  seqof2  14022  ramcl  17000  prdsplusgval  17436  prdsmulrval  17438  prdsvscaval  17442  galactghm  19379  gsum2dlem2  19946  gsum2d  19947  dprdfinv  19996  dprdfadd  19997  dmdprdsplitlem  20014  dpjfval  20032  dpjidcl  20035  mptscmfsupp0  20922  frlmgsum  21752  frlmphllem  21760  psrass1lem  21912  psrridm  21941  psrcom  21946  mvrfval  21959  mplcoe5  22018  mplbas2  22020  evlslem6  22059  evlsvvvallem  22069  evlsvvval  22071  selvffval  22099  psdffval  22123  psdfval  22124  psdmplcl  22128  psdmul  22132  evls1sca  22288  evls1fpws  22334  matgsum  22402  mvmulval  22508  mavmul0g  22518  marepvval0  22531  ptcnplem  23586  xkocnv  23779  ptcmplem3  24019  prdsdsf  24332  ressprdsds  24336  prdsxmslem2  24494  rrx0  25364  tdeglem4  26025  pserulm  26387  efsubm  26515  addsuniflem  27993  suppovss  32754  fisuppov1  32756  mptiffisupp  32766  fsuppcurry1  32797  fsuppcurry2  32798  gsummptres2  33114  gsumfs2d  33122  tocycval  33169  rmfsupp2  33299  elrgspnlem2  33304  elrsp  33432  qusrn  33469  elrspunidl  33488  elrspunsn  33489  extvval  33675  extvfv  33677  extvfvcl  33680  extvfvalf  33681  mplvrpmfgalem  33688  mplvrpmga  33689  mplvrpmmhm  33690  mplvrpmrhm  33691  psrmonmul2  33695  issply  33705  esplyfvaln  33718  drgextgsum  33739  ply1degltdimlem  33766  fedgmullem2  33774  evls1fldgencl  33814  fldextrspunlsplem  33817  fldextrspunlsp  33818  extdgfialglem1  33836  extdgfialglem2  33837  minplyval  33849  ofcfval  34242  lpadval  34820  bj-imdirvallem  37494  qmapex  38772  hashscontpow  42561  aks6d1c2  42569  sticksstones4  42588  sticksstones11  42595  sticksstones12a  42596  sticksstones12  42597  sticksstones17  42602  sticksstones18  42603  sticksstones19  42604  sticksstones20  42605  aks6d1c6lem2  42610  aks6d1c6lem3  42611  aks6d1c7lem2  42620  aks5lem2  42626  selvvvval  43018  evlselv  43020  mhphf  43030  rfovfvd  44429  fsovfvd  44437  dssmapf1od  44448  choicefi  45629  axccdom  45651  climeldmeqmpt  46096  climfveqmpt  46099  climfveqmpt3  46110  climeldmeqmpt3  46117  climfveqmpt2  46121  climeldmeqmpt2  46123  climeqmpt  46125  limsupresicompt  46184  liminfresicompt  46208  liminfvalxr  46211  liminflbuz2  46243  iccvonmbllem  47106  vonioolem1  47108  vonioolem2  47109  vonicclem1  47111  vonicclem2  47112  smflimmpt  47238  smflimsuplem6  47253  cfsetsnfsetfv  47505  cfsetsnfsetf  47506  fundcmpsurbijinjpreimafv  47867  prproropen  47968  isubgr3stgr  48451  uspgrbispr  48627  1arymaptfv  49116  1arymaptfo  49119  fuco22  49814