Theorem mptex 7163

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

Syntax hints:   ∈ wcel 2113  Vcvv 3437   ↦ cmpt 5174

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2705  ax-rep 5219  ax-sep 5236  ax-nul 5246  ax-pr 5372

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2725  df-clel 2808  df-nfc 2882  df-ne 2930  df-ral 3049  df-rex 3058  df-reu 3348  df-rab 3397  df-v 3439  df-sbc 3738  df-csb 3847  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4283  df-if 4475  df-sn 4576  df-pr 4578  df-op 4582  df-uni 4859  df-iun 4943  df-br 5094  df-opab 5156  df-mpt 5175  df-id 5514  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  df-iota 6442  df-fun 6488  df-fn 6489  df-f 6490  df-f1 6491  df-fo 6492  df-f1o 6493  df-fv 6494

This theorem is referenced by:  mptrabex  7165  mptfvmpt  7168  eufnfv  7169  fvresex  7898  ofmres  7922  noinfep  9557  cantnffval  9560  cnfcomlem  9596  cnfcom3clem  9602  ssttrcl  9612  ttrcltr  9613  ttrclselem2  9623  fseqenlem1  9922  dfacacn  10040  dfac12lem1  10042  infmap2  10115  ackbij2lem2  10137  ackbij2lem3  10138  fin23lem32  10242  konigthlem  10466  wunex2  10636  wuncval2  10645  rpnnen1lem1  12878  rpnnen1lem3  12879  rpnnen1lem5  12881  mptnn0fsupp  13906  ccatfn  14481  ccatfval  14482  swrdval  14553  swrd00  14554  swrd0  14568  revval  14669  repsundef  14680  climmpt  15480  climle  15549  iserabs  15724  isumshft  15748  divcnvshft  15764  supcvg  15765  trireciplem  15771  expcnv  15773  explecnv  15774  geolim  15779  geo2lim  15784  cvgrat  15792  mertenslem2  15794  eftlub  16020  rpnnen2lem1  16125  rpnnen2lem2  16126  1arithlem1  16837  1arith  16841  vdwapval  16887  vdwlem6  16900  vdwlem9  16903  restfn  17330  cidffn  17586  idfu2nd  17786  idfu1st  17788  idfucl  17790  fucco  17874  homafval  17938  prf1  18108  prf2fval  18109  prfcl  18111  prf1st  18112  prf2nd  18113  curf1fval  18132  curf11  18134  curf12  18135  curf1cl  18136  curf2  18137  curfcl  18140  hof2val  18164  yonedalem3a  18182  yonedalem4a  18183  yonedalem4b  18184  yonedalem4c  18185  yonedalem3  18188  yonedainv  18189  lubfval  18256  glbfval  18269  smndex1gbas  18812  smndex1gid  18813  smndex1igid  18814  smndex1mnd  18820  smndex1id  18821  smndex1n0mnd  18822  smndex2dbas  18824  smndex2hbas  18826  cntzfval  19234  psgnfval  19414  sylow1lem2  19513  sylow2blem1  19534  sylow2blem2  19535  sylow3lem1  19541  sylow3lem6  19546  pj1fval  19608  vrgpfval  19680  rgspnval  20529  lspfval  20908  sraval  21111  irinitoringc  21418  zrhval2  21447  aspval  21812  psrmulfval  21882  psrass1  21902  mvrval  21920  mplmon  21971  mplcoe1  21973  evlslem2  22015  mpfrcl  22021  evlsval  22022  evlsvar  22026  mpfind  22043  mhpfval  22054  psdval  22075  psdmul  22082  coe1fval  22119  psropprmul  22151  coe1mul2  22184  ply1coe  22214  evls1fval  22235  evls1val  22236  evl1fval  22244  evl1val  22245  submafval  22495  mdetfval  22502  madufval  22553  minmar1fval  22562  pmatcollpw2lem  22693  pm2mpval  22711  1stcfb  23361  ptbasfi  23497  dfac14  23534  fmval  23859  fmf  23861  flffval  23905  fcfval  23949  cnextval  23977  met1stc  24437  pcoval  24939  iscmet3lem3  25218  rrxsca  25324  mbflimsup  25595  mbflim  25597  itg1climres  25643  mbfi1fseqlem2  25645  mbfi1fseqlem4  25647  mbfi1fseqlem6  25649  mbfi1flimlem  25651  mbfmullem2  25653  itg2monolem1  25679  itg2addlem  25687  itg2cnlem1  25690  cpnfval  25862  mdegfval  25995  elply  26128  plyeq0lem  26143  plypf1  26145  geolim3  26275  ulmuni  26329  ulmcau  26332  ulmdvlem1  26337  ulmdvlem3  26339  mbfulm  26343  itgulm  26345  pserval  26347  dvradcnv  26358  pserdvlem2  26366  abelthlem1  26369  abelthlem3  26371  abelthlem6  26374  logtayl  26597  leibpi  26880  dfef2  26909  emcllem4  26937  emcllem6  26939  emcllem7  26940  lgamgulmlem5  26971  lgamgulmlem6  26972  lgamcvg2  26993  basellem6  27024  sqff1o  27120  dchrptlem2  27204  dchrptlem3  27205  2lgslem1  27333  dchrisumlem3  27430  padicfval  27555  padicabvf  27570  istrkg2ld  28439  mirval  28634  ishpg  28738  lmif  28764  islmib  28766  axlowdim  28941  crctcshlem3  29799  nmoofval  30744  pjhfval  31378  pjmfn  31697  hosmval  31717  hommval  31718  hodmval  31719  hfsmval  31720  hfmmval  31721  eigvalfval  31879  brafval  31925  kbfval  31934  rnbra  32089  bra11  32090  padct  32705  fpwrelmap  32720  qusima  33380  nsgmgc  33384  nsgqusf1o  33388  idlsrgtset  33480  extvfval  33583  mplvrpmga  33593  esplyval  33603  locfinreflem  33874  rspectopn  33901  zarcmplem  33915  ordtconnlem1  33958  xrhval  34052  sigapildsys  34196  sxbrsigalem2  34320  eulerpart  34416  dstfrvclim1  34512  ballotlemfval  34524  ballotlemsval  34543  signstfv  34597  vtsval  34671  fineqvnttrclse  35165  cvmliftlem5  35354  mrsubffval  35572  mrsubfval  35573  msubffval  35588  msubfval  35589  msubrn  35594  msubco  35596  msubvrs  35625  circum  35739  divcnvlin  35798  climlec3  35799  faclimlem2  35809  faclim2  35813  knoppcnlem1  36558  knoppcnlem6  36563  knoppcnlem7  36564  cnndvlem2  36603  bj-endval  37380  ptrest  37679  poimirlem17  37697  poimirlem20  37700  voliunnfl  37724  volsupnfl  37725  upixp  37789  sdclem2  37802  fdc  37805  lmclim2  37818  geomcau  37819  rrncmslem  37892  pclfvalN  40008  polfvalN  40023  trlset  40280  tendopl  40895  docafvalN  41241  dibfval  41260  dibopelvalN  41262  dibopelval2  41264  dibelval3  41266  dibn0  41272  dib0  41283  diblsmopel  41290  dicn0  41311  dihopelvalcpre  41367  dihatlat  41453  dihpN  41455  dochfval  41469  lcfrlem9  41669  hvmapfval  41878  hvmapval  41879  hdmap1fval  41915  hlhilset  42053  sticksstones10  42268  sticksstones12a  42270  aks6d1c6isolem2  42288  evlsvvvallem2  42680  evlsvvval  42681  selvvvval  42703  evlselv  42705  prjcrvfval  42749  mzpincl  42851  dfac11  43179  dfac21  43183  hbtlem1  43240  hbtlem7  43242  fsovd  44125  mnringmulrcld  44345  dvgrat  44429  radcnvrat  44431  hashnzfzclim  44439  uzmptshftfval  44463  dvradcnv2  44464  binomcxplemrat  44467  binomcxplemcvg  44471  binomcxplemdvsum  44472  binomcxplemnotnn0  44473  addrval  44582  subrval  44583  mulvval  44584  fmuldfeqlem1  45706  fmuldfeq  45707  clim1fr1  45725  climexp  45729  climneg  45734  climdivf  45736  divcnvg  45751  expfac  45779  climresmpt  45781  climsubmpt  45782  limsupval4  45916  climliminflimsupd  45923  liminfreuzlem  45924  liminfltlem  45926  liminfpnfuz  45938  dvsinax  46035  dvcosax  46048  ioodvbdlimc1lem2  46054  ioodvbdlimc2lem  46056  dvnprodlem1  46068  dvnprodlem2  46069  dvnprodlem3  46070  stoweidlem59  46181  wallispilem5  46191  wallispi  46192  stirlinglem1  46196  stirlinglem8  46203  stirlinglem14  46209  stirlinglem15  46210  dirkerval  46213  fourierdlem71  46299  fourierdlem103  46331  fourierdlem104  46332  fourierdlem112  46340  etransclem48  46404  salgensscntex  46466  sge0tsms  46502  nnfoctbdjlem  46577  isomenndlem  46652  ovnval  46663  ovncvrrp  46686  ovnsubaddlem1  46692  hsphoif  46698  hsphoival  46701  ovnhoilem2  46724  hoidifhspval  46730  ovncvr2  46733  hspmbllem2  46749  vonioolem1  46802  smfpimcclem  46929  smflimsuplem1  46942  smflimsuplem4  46945  smflimsuplem7  46948  smfliminflem  46952  fsupdm  46964  smfsupdmmbllem  46966  finfdm  46968  smfinfdmmbllem  46970  cfsetsnfsetfo  47184  isuspgrim0  48018  cycldlenngric  48052  isgrtri  48067  1aryenef  48770  2aryenef  48781  itcovalpclem2  48796  itcovalt2lem2  48801  ackvalsuc1mpt  48803  ackval0  48805  cofidvala  49241  cofidval  49244  isnatd  49348  swapfelvv  49388  swapf2fvala  49389  swapf1vala  49391  swapf2fn  49393  swapf2vala  49395  tposcurf1  49424  prcofelvv  49505  reldmprcof1  49506  reldmprcof2  49507  prcof1  49513  prcof2a  49514  prcof2  49515  idfudiag1bas  49649  idfudiag1  49650  lmdfval  49774  cmdfval  49775  aacllem  49926