Theorem mptex 7243

Description: If the domain of a function given by maps-to notation is a set, the function is a set. Inference version of mptexg 7241. (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 7241	. 2 ⊢ (𝐴 ∈ V → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ V)
3	1, 2	ax-mp 5	1 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ V

Syntax hints:   ∈ wcel 2108  Vcvv 3480   ↦ cmpt 5225

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 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-rep 5279  ax-sep 5296  ax-nul 5306  ax-pr 5432

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-ral 3062  df-rex 3071  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-iun 4993  df-br 5144  df-opab 5206  df-mpt 5226  df-id 5578  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569

This theorem is referenced by:  mptrabex  7245  mptfvmpt  7248  eufnfv  7249  fvresex  7984  ofmres  8009  noinfep  9700  cantnffval  9703  cnfcomlem  9739  cnfcom3clem  9745  ssttrcl  9755  ttrcltr  9756  ttrclselem2  9766  fseqenlem1  10064  dfacacn  10182  dfac12lem1  10184  infmap2  10257  ackbij2lem2  10279  ackbij2lem3  10280  fin23lem32  10384  konigthlem  10608  wunex2  10778  wuncval2  10787  rpnnen1lem1  13020  rpnnen1lem3  13021  rpnnen1lem5  13023  mptnn0fsupp  14038  ccatfn  14610  ccatfval  14611  swrdval  14681  swrd00  14682  swrd0  14696  revval  14798  repsundef  14809  climmpt  15607  climle  15676  iserabs  15851  isumshft  15875  divcnvshft  15891  supcvg  15892  trireciplem  15898  expcnv  15900  explecnv  15901  geolim  15906  geo2lim  15911  cvgrat  15919  mertenslem2  15921  eftlub  16145  rpnnen2lem1  16250  rpnnen2lem2  16251  1arithlem1  16961  1arith  16965  vdwapval  17011  vdwlem6  17024  vdwlem9  17027  restfn  17469  cidffn  17721  idfu2nd  17922  idfu1st  17924  idfucl  17926  fucco  18010  homafval  18074  prf1  18245  prf2fval  18246  prfcl  18248  prf1st  18249  prf2nd  18250  curf1fval  18269  curf11  18271  curf12  18272  curf1cl  18273  curf2  18274  curfcl  18277  hof2val  18301  yonedalem3a  18319  yonedalem4a  18320  yonedalem4b  18321  yonedalem4c  18322  yonedalem3  18325  yonedainv  18326  lubfval  18395  glbfval  18408  smndex1gbas  18915  smndex1gid  18916  smndex1igid  18917  smndex1mnd  18923  smndex1id  18924  smndex1n0mnd  18925  smndex2dbas  18927  smndex2hbas  18929  cntzfval  19338  psgnfval  19518  sylow1lem2  19617  sylow2blem1  19638  sylow2blem2  19639  sylow3lem1  19645  sylow3lem6  19650  pj1fval  19712  vrgpfval  19784  rgspnval  20612  lspfval  20971  sraval  21174  irinitoringc  21490  zrhval2  21519  aspval  21893  psrmulfval  21963  psrass1  21984  mvrval  22002  mplmon  22053  mplcoe1  22055  evlslem2  22103  mpfrcl  22109  evlsval  22110  evlsvar  22114  mpfind  22131  mhpfval  22142  psdval  22163  psdmul  22170  coe1fval  22207  psropprmul  22239  coe1mul2  22272  ply1coe  22302  evls1fval  22323  evls1val  22324  evl1fval  22332  evl1val  22333  submafval  22585  mdetfval  22592  madufval  22643  minmar1fval  22652  pmatcollpw2lem  22783  pm2mpval  22801  1stcfb  23453  ptbasfi  23589  dfac14  23626  fmval  23951  fmf  23953  flffval  23997  fcfval  24041  cnextval  24069  met1stc  24534  pcoval  25044  iscmet3lem3  25324  rrxsca  25430  mbflimsup  25701  mbflim  25703  itg1climres  25749  mbfi1fseqlem2  25751  mbfi1fseqlem4  25753  mbfi1fseqlem6  25755  mbfi1flimlem  25757  mbfmullem2  25759  itg2monolem1  25785  itg2addlem  25793  itg2cnlem1  25796  cpnfval  25968  mdegfval  26101  elply  26234  plyeq0lem  26249  plypf1  26251  geolim3  26381  ulmuni  26435  ulmcau  26438  ulmdvlem1  26443  ulmdvlem3  26445  mbfulm  26449  itgulm  26451  pserval  26453  dvradcnv  26464  pserdvlem2  26472  abelthlem1  26475  abelthlem3  26477  abelthlem6  26480  logtayl  26702  leibpi  26985  dfef2  27014  emcllem4  27042  emcllem6  27044  emcllem7  27045  lgamgulmlem5  27076  lgamgulmlem6  27077  lgamcvg2  27098  basellem6  27129  sqff1o  27225  dchrptlem2  27309  dchrptlem3  27310  2lgslem1  27438  dchrisumlem3  27535  padicfval  27660  padicabvf  27675  istrkg2ld  28468  mirval  28663  ishpg  28767  lmif  28793  islmib  28795  axlowdim  28976  crctcshlem3  29839  nmoofval  30781  pjhfval  31415  pjmfn  31734  hosmval  31754  hommval  31755  hodmval  31756  hfsmval  31757  hfmmval  31758  eigvalfval  31916  brafval  31962  kbfval  31971  rnbra  32126  bra11  32127  padct  32731  fpwrelmap  32744  qusima  33436  nsgmgc  33440  nsgqusf1o  33444  idlsrgtset  33536  locfinreflem  33839  rspectopn  33866  zarcmplem  33880  ordtconnlem1  33923  xrhval  34019  sigapildsys  34163  sxbrsigalem2  34288  eulerpart  34384  dstfrvclim1  34480  ballotlemfval  34492  ballotlemsval  34511  signstfv  34578  vtsval  34652  cvmliftlem5  35294  mrsubffval  35512  mrsubfval  35513  msubffval  35528  msubfval  35529  msubrn  35534  msubco  35536  msubvrs  35565  circum  35679  divcnvlin  35733  climlec3  35734  faclimlem2  35744  faclim2  35748  knoppcnlem1  36494  knoppcnlem6  36499  knoppcnlem7  36500  cnndvlem2  36539  bj-endval  37316  ptrest  37626  poimirlem17  37644  poimirlem20  37647  voliunnfl  37671  volsupnfl  37672  upixp  37736  sdclem2  37749  fdc  37752  lmclim2  37765  geomcau  37766  rrncmslem  37839  pclfvalN  39891  polfvalN  39906  trlset  40163  tendopl  40778  docafvalN  41124  dibfval  41143  dibopelvalN  41145  dibopelval2  41147  dibelval3  41149  dibn0  41155  dib0  41166  diblsmopel  41173  dicn0  41194  dihopelvalcpre  41250  dihatlat  41336  dihpN  41338  dochfval  41352  lcfrlem9  41552  hvmapfval  41761  hvmapval  41762  hdmap1fval  41798  hlhilset  41936  sticksstones10  42156  sticksstones12a  42158  aks6d1c6isolem2  42176  evlsvvvallem2  42572  evlsvvval  42573  selvvvval  42595  evlselv  42597  prjcrvfval  42641  mzpincl  42745  dfac11  43074  dfac21  43078  hbtlem1  43135  hbtlem7  43137  fsovd  44021  mnringmulrcld  44247  dvgrat  44331  radcnvrat  44333  hashnzfzclim  44341  uzmptshftfval  44365  dvradcnv2  44366  binomcxplemrat  44369  binomcxplemcvg  44373  binomcxplemdvsum  44374  binomcxplemnotnn0  44375  addrval  44485  subrval  44486  mulvval  44487  fmuldfeqlem1  45597  fmuldfeq  45598  clim1fr1  45616  climexp  45620  climneg  45625  climdivf  45627  divcnvg  45642  expfac  45672  climresmpt  45674  climsubmpt  45675  limsupval4  45809  climliminflimsupd  45816  liminfreuzlem  45817  liminfltlem  45819  liminfpnfuz  45831  dvsinax  45928  dvcosax  45941  ioodvbdlimc1lem2  45947  ioodvbdlimc2lem  45949  dvnprodlem1  45961  dvnprodlem2  45962  dvnprodlem3  45963  stoweidlem59  46074  wallispilem5  46084  wallispi  46085  stirlinglem1  46089  stirlinglem8  46096  stirlinglem14  46102  stirlinglem15  46103  dirkerval  46106  fourierdlem71  46192  fourierdlem103  46224  fourierdlem104  46225  fourierdlem112  46233  etransclem48  46297  salgensscntex  46359  sge0tsms  46395  nnfoctbdjlem  46470  isomenndlem  46545  ovnval  46556  ovncvrrp  46579  ovnsubaddlem1  46585  hsphoif  46591  hsphoival  46594  ovnhoilem2  46617  hoidifhspval  46623  ovncvr2  46626  hspmbllem2  46642  vonioolem1  46695  smfpimcclem  46822  smflimsuplem1  46835  smflimsuplem4  46838  smflimsuplem7  46841  smfliminflem  46845  fsupdm  46857  smfsupdmmbllem  46859  finfdm  46861  smfinfdmmbllem  46863  cfsetsnfsetfo  47072  isuspgrim0  47872  isgrtri  47910  1aryenef  48566  2aryenef  48577  itcovalpclem2  48592  itcovalt2lem2  48597  ackvalsuc1mpt  48599  ackval0  48601  isnatd  48949  swapfelvv  48969  swapf2fvala  48970  swapf1vala  48972  swapf2fn  48974  swapf2vala  48976  tposcurf1  48999  aacllem  49320