Theorem mptexd 7082

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

Syntax hints:   → wi 4   ∈ wcel 2108  Vcvv 3422   ↦ cmpt 5153

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-rep 5205  ax-sep 5218  ax-nul 5225  ax-pr 5347

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-ral 3068  df-rex 3069  df-reu 3070  df-rab 3072  df-v 3424  df-sbc 3712  df-csb 3829  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-iun 4923  df-br 5071  df-opab 5133  df-mpt 5154  df-id 5480  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-res 5592  df-ima 5593  df-iota 6376  df-fun 6420  df-fn 6421  df-f 6422  df-f1 6423  df-fo 6424  df-f1o 6425  df-fv 6426

This theorem is referenced by:  mptsuppdifd  7973  mpocurryvald  8057  fsetfocdm  8607  fsuppmptif  9088  sniffsupp  9089  cantnfrescl  9364  cantnflem1  9377  infxpenc2lem2  9707  ac5num  9723  ac6num  10166  negfi  11854  seqof2  13709  ramcl  16658  prdsplusgval  17101  prdsmulrval  17103  prdsvscaval  17107  galactghm  18927  gsum2dlem2  19487  gsum2d  19488  dprdfinv  19537  dprdfadd  19538  dmdprdsplitlem  19555  dpjfval  19573  dpjidcl  19576  mptscmfsupp0  20103  frlmgsum  20889  frlmphllem  20897  psrass1lemOLD  21053  psrass1lem  21056  psrridm  21083  psrcom  21088  mvrfval  21099  mplcoe5  21151  mplbas2  21153  evlslem6  21201  selvffval  21236  evls1sca  21399  matgsum  21494  mvmulval  21600  mavmul0g  21610  marepvval0  21623  ptcnplem  22680  xkocnv  22873  ptcmplem3  23113  prdsdsf  23428  ressprdsds  23432  prdsxmslem2  23591  rrx0  24466  tdeglem4  25129  tdeglem4OLD  25130  pserulm  25486  efsubm  25612  suppovss  30919  fsuppcurry1  30962  fsuppcurry2  30963  gsummptres2  31215  tocycval  31277  rmfsupp2  31394  elrsp  31471  elrspunidl  31508  drgextgsum  31584  fedgmullem2  31613  ofcfval  31966  lpadval  32556  bj-imdirvallem  35278  sticksstones4  40033  sticksstones11  40040  sticksstones12a  40041  sticksstones12  40042  sticksstones17  40047  sticksstones18  40048  sticksstones19  40049  sticksstones20  40050  evlsbagval  40198  mhphf  40208  rfovfvd  41499  fsovfvd  41507  dssmapf1od  41518  choicefi  42629  axccdom  42651  climeldmeqmpt  43099  climfveqmpt  43102  climfveqmpt3  43113  climeldmeqmpt3  43120  climfveqmpt2  43124  climeldmeqmpt2  43126  climeqmpt  43128  limsupresicompt  43187  liminfresicompt  43211  liminfvalxr  43214  liminflbuz2  43246  iccvonmbllem  44106  vonioolem1  44108  vonioolem2  44109  vonicclem1  44111  vonicclem2  44112  smflimmpt  44230  smflimsuplem6  44245  cfsetsnfsetfv  44438  cfsetsnfsetf  44439  fundcmpsurbijinjpreimafv  44747  prproropen  44848  uspgrbispr  45201  1arymaptfv  45874  1arymaptfo  45877