Theorem mptexd 7212

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

Syntax hints:   → wi 4   ∈ wcel 2145  Vcvv 3457   ↦ cmpt 5185

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2737  ax-rep 5231  ax-sep 5250  ax-nul 5260  ax-pr 5394

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-nf 1807  df-sb 2094  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-ral 3080  df-rex 3090  df-reu 3371  df-rab 3418  df-v 3459  df-sbc 3748  df-csb 3856  df-dif 3910  df-un 3912  df-in 3914  df-ss 3924  df-nul 4289  df-if 4484  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-iun 4953  df-br 5105  df-opab 5167  df-mpt 5186  df-id 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-iota 6481  df-fun 6527  df-fn 6528  df-f 6529  df-f1 6530  df-fo 6531  df-f1o 6532  df-fv 6533

This theorem is referenced by:  mptsuppdifd  8170  mpocurryvald  8254  fsetfocdm  8846  fsuppssov1  9332  fsuppmptif  9347  sniffsupp  9348  cantnfrescl  9633  cantnflem1  9646  infxpenc2lem2  9992  ac5num  10008  ac6num  10451  negfi  12152  seqof2  14084  ramcl  17077  prdsplusgval  17514  prdsmulrval  17516  prdsvscaval  17520  galactghm  19462  gsum2dlem2  20029  gsum2d  20030  dprdfinv  20079  dprdfadd  20080  dmdprdsplitlem  20097  dpjfval  20115  dpjidcl  20118  mptscmfsupp0  21014  frlmgsum  21879  frlmphllem  21887  psrass1lem  22040  psrridm  22069  psrcom  22074  mvrfval  22087  mplcoe5  22148  mplbas2  22150  evlslem6  22189  evlsvvvallem  22199  evlsvvval  22201  selvffval  22226  selvvvval  22250  psdffval  22277  psdfval  22278  psdmplcl  22282  psdmul  22286  evls1sca  22440  evls1fpws  22486  matgsum  22551  mvmulval  22657  mavmul0g  22667  marepvval0  22680  ptcnplem  23735  xkocnv  23928  ptcmplem3  24168  prdsdsf  24481  ressprdsds  24485  prdsxmslem2  24643  rrx0  25513  tdeglem4  26174  pserulm  26539  efsubm  26670  addsuniflem  28148  suppovss  32934  fisuppov1  32936  mptiffisupp  32946  fsuppcurry1  32977  fsuppcurry2  32978  gsummptres2  33281  gsumfs2d  33289  tocycval  33336  rmfsupp2  33465  elrgspnlem2  33471  elrsp  33596  qusrn  33629  elrspunidl  33647  elrspunsn  33648  selvply1rhmlema  33820  selvply1rhmlemb  33821  selvply1rhmlem3  33824  selvply1rhmlem4  33825  selvply1rhmlem5  33826  extvval  33833  extvfv  33835  extvfvcl  33838  extvfvalf  33839  mplvrpmfgalem  33846  mplvrpmga  33847  mplvrpmmhm  33848  mplvrpmrhm  33849  psrmonmul2  33853  issply  33863  esplyfvaln  33876  drgextgsum  33897  ply1degltdimlem  33924  fedgmullem2  33932  evls1fldgencl  33972  fldextrspunlsplem  33975  fldextrspunlsp  33976  extdgfialglem1  33994  extdgfialglem2  33995  minplyval  34007  ofcfval  34400  lpadval  34978  bj-imdirvallem  37679  qmapex  38957  hashscontpow  42746  aks6d1c2  42754  sticksstones4  42773  sticksstones11  42780  sticksstones12a  42781  sticksstones12  42782  sticksstones17  42787  sticksstones18  42788  sticksstones19  42789  sticksstones20  42790  aks6d1c6lem2  42795  aks6d1c6lem3  42796  aks6d1c7lem2  42805  aks5lem2  42811  evlselv  43178  mhphf  43186  rfovfvd  44585  fsovfvd  44593  dssmapf1od  44604  choicefi  45776  axccdom  45797  climeldmeqmpt  46241  climfveqmpt  46244  climfveqmpt3  46255  climeldmeqmpt3  46262  climfveqmpt2  46266  climeldmeqmpt2  46268  climeqmpt  46270  limsupresicompt  46329  liminfresicompt  46353  liminfvalxr  46356  liminflbuz2  46388  iccvonmbllem  47251  vonioolem1  47253  vonioolem2  47254  vonicclem1  47256  vonicclem2  47257  smflimmpt  47383  smflimsuplem6  47398  cfsetsnfsetfv  47650  cfsetsnfsetf  47651  fundcmpsurbijinjpreimafv  48012  prproropen  48113  isubgr3stgr  48596  uspgrbispr  48772  1arymaptfv  49272  1arymaptfo  49275  fuco22  49969