Theorem mptex 7108

Description: If the domain of a function given by maps-to notation is a set, the function is a set. Inference version of mptexg 7106. (Contributed by NM, 22-Apr-2005.) (Revised by Mario Carneiro, 20-Dec-2013.)

Hypothesis

Ref	Expression
mptex.1	⊢ 𝐴 ∈ V

Assertion

Ref	Expression
mptex	⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ V

Distinct variable group:   𝑥,𝐴

Allowed substitution hint:   𝐵(𝑥)

Proof of Theorem mptex

Step	Hyp	Ref	Expression
1		mptex.1	. 2 ⊢ 𝐴 ∈ V
2		mptexg 7106	. 2 ⊢ (𝐴 ∈ V → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ V)
3	1, 2	ax-mp 5	1 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ V

Syntax hints:   ∈ wcel 2107  Vcvv 3433   ↦ cmpt 5158

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2710  ax-rep 5210  ax-sep 5224  ax-nul 5231  ax-pr 5353

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-nfc 2890  df-ne 2945  df-ral 3070  df-rex 3071  df-reu 3073  df-rab 3074  df-v 3435  df-sbc 3718  df-csb 3834  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-nul 4258  df-if 4461  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4841  df-iun 4927  df-br 5076  df-opab 5138  df-mpt 5159  df-id 5490  df-xp 5596  df-rel 5597  df-cnv 5598  df-co 5599  df-dm 5600  df-rn 5601  df-res 5602  df-ima 5603  df-iota 6395  df-fun 6439  df-fn 6440  df-f 6441  df-f1 6442  df-fo 6443  df-f1o 6444  df-fv 6445

This theorem is referenced by:  mptrabex  7110  mptfvmpt  7113  eufnfv  7114  fvresex  7811  ofmres  7836  noinfep  9427  cantnffval  9430  cnfcomlem  9466  cnfcom3clem  9472  ssttrcl  9482  ttrcltr  9483  ttrclselem2  9493  fseqenlem1  9789  dfacacn  9906  dfac12lem1  9908  infmap2  9983  ackbij2lem2  10005  ackbij2lem3  10006  fin23lem32  10109  konigthlem  10333  wunex2  10503  wuncval2  10512  rpnnen1lem1  12727  rpnnen1lem3  12728  rpnnen1lem5  12730  mptnn0fsupp  13726  ccatfn  14284  ccatfval  14285  swrdval  14365  swrd00  14366  swrd0  14380  revval  14482  repsundef  14493  climmpt  15289  climle  15358  iserabs  15536  isumshft  15560  divcnvshft  15576  supcvg  15577  trireciplem  15583  expcnv  15585  explecnv  15586  geolim  15591  geo2lim  15596  cvgrat  15604  mertenslem2  15606  eftlub  15827  rpnnen2lem1  15932  rpnnen2lem2  15933  1arithlem1  16633  1arith  16637  vdwapval  16683  vdwlem6  16696  vdwlem9  16699  restfn  17144  cidffn  17396  idfu2nd  17601  idfu1st  17603  idfucl  17605  fucco  17689  homafval  17753  prf1  17926  prf2fval  17927  prfcl  17929  prf1st  17930  prf2nd  17931  curf1fval  17951  curf11  17953  curf12  17954  curf1cl  17955  curf2  17956  curfcl  17959  hof2val  17983  yonedalem3a  18001  yonedalem4a  18002  yonedalem4b  18003  yonedalem4c  18004  yonedalem3  18007  yonedainv  18008  lubfval  18077  glbfval  18090  smndex1gbas  18550  smndex1gid  18551  smndex1igid  18552  smndex1mnd  18558  smndex1id  18559  smndex1n0mnd  18560  smndex2dbas  18562  smndex2hbas  18564  cntzfval  18935  psgnfval  19117  sylow1lem2  19213  sylow2blem1  19234  sylow2blem2  19235  sylow3lem1  19241  sylow3lem6  19246  pj1fval  19309  vrgpfval  19381  lspfval  20244  sraval  20447  zrhval2  20719  aspval  21086  psrmulfval  21163  psrass1  21183  mvrval  21199  mplmon  21245  mplcoe1  21247  evlslem2  21298  mpfrcl  21304  evlsval  21305  evlsvar  21309  mpfind  21326  mhpfval  21338  coe1fval  21385  psropprmul  21418  coe1mul2  21449  ply1coe  21476  evls1fval  21494  evls1val  21495  evl1fval  21503  evl1val  21504  submafval  21737  mdetfval  21744  madufval  21795  minmar1fval  21804  pmatcollpw2lem  21935  pm2mpval  21953  1stcfb  22605  ptbasfi  22741  dfac14  22778  fmval  23103  fmf  23105  flffval  23149  fcfval  23193  cnextval  23221  met1stc  23686  pcoval  24183  iscmet3lem3  24463  rrxsca  24569  mbflimsup  24839  mbflim  24841  itg1climres  24888  mbfi1fseqlem2  24890  mbfi1fseqlem4  24892  mbfi1fseqlem6  24894  mbfi1flimlem  24896  mbfmullem2  24898  itg2monolem1  24924  itg2addlem  24932  itg2cnlem1  24935  cpnfval  25105  mdegfval  25236  elply  25365  plyeq0lem  25380  plypf1  25382  geolim3  25508  ulmuni  25560  ulmcau  25563  ulmdvlem1  25568  ulmdvlem3  25570  mbfulm  25574  itgulm  25576  pserval  25578  dvradcnv  25589  pserdvlem2  25596  abelthlem1  25599  abelthlem3  25601  abelthlem6  25604  logtayl  25824  leibpi  26101  dfef2  26129  emcllem4  26157  emcllem6  26159  emcllem7  26160  lgamgulmlem5  26191  lgamgulmlem6  26192  lgamcvg2  26213  basellem6  26244  sqff1o  26340  dchrptlem2  26422  dchrptlem3  26423  2lgslem1  26551  dchrisumlem3  26648  padicfval  26773  padicabvf  26788  istrkg2ld  26830  mirval  27025  ishpg  27129  lmif  27155  islmib  27157  axlowdim  27338  crctcshlem3  28193  nmoofval  29133  pjhfval  29767  pjmfn  30086  hosmval  30106  hommval  30107  hodmval  30108  hfsmval  30109  hfmmval  30110  eigvalfval  30268  brafval  30314  kbfval  30323  rnbra  30478  bra11  30479  padct  31063  fpwrelmap  31077  qusima  31603  nsgmgc  31606  nsgqusf1o  31610  idlsrgtset  31662  locfinreflem  31799  rspectopn  31826  zarcmplem  31840  ordtconnlem1  31883  xrhval  31977  sigapildsys  32139  sxbrsigalem2  32262  eulerpart  32358  dstfrvclim1  32453  ballotlemfval  32465  ballotlemsval  32484  signstfv  32551  vtsval  32626  cvmliftlem5  33260  mrsubffval  33478  mrsubfval  33479  msubffval  33494  msubfval  33495  msubrn  33500  msubco  33502  msubvrs  33531  circum  33641  divcnvlin  33707  climlec3  33708  faclimlem2  33719  faclim2  33723  knoppcnlem1  34682  knoppcnlem6  34687  knoppcnlem7  34688  cnndvlem2  34727  bj-endval  35495  ptrest  35785  poimirlem17  35803  poimirlem20  35806  voliunnfl  35830  volsupnfl  35831  upixp  35896  sdclem2  35909  fdc  35912  lmclim2  35925  geomcau  35926  rrncmslem  35999  pclfvalN  37910  polfvalN  37925  trlset  38182  tendopl  38797  docafvalN  39143  dibfval  39162  dibopelvalN  39164  dibopelval2  39166  dibelval3  39168  dibn0  39174  dib0  39185  diblsmopel  39192  dicn0  39213  dihopelvalcpre  39269  dihatlat  39355  dihpN  39357  dochfval  39371  lcfrlem9  39571  hvmapfval  39780  hvmapval  39781  hdmap1fval  39817  hlhilset  39955  sticksstones10  40118  sticksstones12a  40120  evlsbagval  40282  mhphf  40292  prjcrvfval  40475  mzpincl  40563  dfac11  40894  dfac21  40898  hbtlem1  40955  hbtlem7  40957  rgspnval  41000  fsovd  41623  mnringmulrcld  41853  dvgrat  41937  radcnvrat  41939  hashnzfzclim  41947  uzmptshftfval  41971  dvradcnv2  41972  binomcxplemrat  41975  binomcxplemcvg  41979  binomcxplemdvsum  41980  binomcxplemnotnn0  41981  addrval  42091  subrval  42092  mulvval  42093  fmuldfeqlem1  43130  fmuldfeq  43131  clim1fr1  43149  climexp  43153  climneg  43158  climdivf  43160  divcnvg  43175  expfac  43205  climresmpt  43207  climsubmpt  43208  limsupval4  43342  climliminflimsupd  43349  liminfreuzlem  43350  liminfltlem  43352  liminfpnfuz  43364  dvsinax  43461  dvcosax  43474  ioodvbdlimc1lem2  43480  ioodvbdlimc2lem  43482  dvnprodlem1  43494  dvnprodlem2  43495  dvnprodlem3  43496  stoweidlem59  43607  wallispilem5  43617  wallispi  43618  stirlinglem1  43622  stirlinglem8  43629  stirlinglem14  43635  stirlinglem15  43636  dirkerval  43639  fourierdlem71  43725  fourierdlem103  43757  fourierdlem104  43758  fourierdlem112  43766  etransclem48  43830  salgensscntex  43890  sge0tsms  43925  nnfoctbdjlem  44000  isomenndlem  44075  ovnval  44086  ovncvrrp  44109  ovnsubaddlem1  44115  hsphoif  44121  hsphoival  44124  ovnhoilem2  44147  hoidifhspval  44153  ovncvr2  44156  hspmbllem2  44172  vonioolem1  44225  smfpimcclem  44351  smflimsuplem1  44364  smflimsuplem4  44367  smflimsuplem7  44370  smfliminflem  44374  cfsetsnfsetfo  44565  isomuspgrlem2  45296  irinitoringc  45638  1aryenef  46002  2aryenef  46013  itcovalpclem2  46028  itcovalt2lem2  46033  ackvalsuc1mpt  46035  ackval0  46037  aacllem  46516