Theorem mptex 7157

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

Syntax hints:   ∈ wcel 2111  Vcvv 3436   ↦ cmpt 5172

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 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-rep 5217  ax-sep 5234  ax-nul 5244  ax-pr 5370

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 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-ral 3048  df-rex 3057  df-reu 3347  df-rab 3396  df-v 3438  df-sbc 3742  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4284  df-if 4476  df-sn 4577  df-pr 4579  df-op 4583  df-uni 4860  df-iun 4943  df-br 5092  df-opab 5154  df-mpt 5173  df-id 5511  df-xp 5622  df-rel 5623  df-cnv 5624  df-co 5625  df-dm 5626  df-rn 5627  df-res 5628  df-ima 5629  df-iota 6437  df-fun 6483  df-fn 6484  df-f 6485  df-f1 6486  df-fo 6487  df-f1o 6488  df-fv 6489

This theorem is referenced by:  mptrabex  7159  mptfvmpt  7162  eufnfv  7163  fvresex  7892  ofmres  7916  noinfep  9550  cantnffval  9553  cnfcomlem  9589  cnfcom3clem  9595  ssttrcl  9605  ttrcltr  9606  ttrclselem2  9616  fseqenlem1  9912  dfacacn  10030  dfac12lem1  10032  infmap2  10105  ackbij2lem2  10127  ackbij2lem3  10128  fin23lem32  10232  konigthlem  10456  wunex2  10626  wuncval2  10635  rpnnen1lem1  12873  rpnnen1lem3  12874  rpnnen1lem5  12876  mptnn0fsupp  13901  ccatfn  14476  ccatfval  14477  swrdval  14548  swrd00  14549  swrd0  14563  revval  14664  repsundef  14675  climmpt  15475  climle  15544  iserabs  15719  isumshft  15743  divcnvshft  15759  supcvg  15760  trireciplem  15766  expcnv  15768  explecnv  15769  geolim  15774  geo2lim  15779  cvgrat  15787  mertenslem2  15789  eftlub  16015  rpnnen2lem1  16120  rpnnen2lem2  16121  1arithlem1  16832  1arith  16836  vdwapval  16882  vdwlem6  16895  vdwlem9  16898  restfn  17325  cidffn  17581  idfu2nd  17781  idfu1st  17783  idfucl  17785  fucco  17869  homafval  17933  prf1  18103  prf2fval  18104  prfcl  18106  prf1st  18107  prf2nd  18108  curf1fval  18127  curf11  18129  curf12  18130  curf1cl  18131  curf2  18132  curfcl  18135  hof2val  18159  yonedalem3a  18177  yonedalem4a  18178  yonedalem4b  18179  yonedalem4c  18180  yonedalem3  18183  yonedainv  18184  lubfval  18251  glbfval  18264  smndex1gbas  18807  smndex1gid  18808  smndex1igid  18809  smndex1mnd  18815  smndex1id  18816  smndex1n0mnd  18817  smndex2dbas  18819  smndex2hbas  18821  cntzfval  19230  psgnfval  19410  sylow1lem2  19509  sylow2blem1  19530  sylow2blem2  19531  sylow3lem1  19537  sylow3lem6  19542  pj1fval  19604  vrgpfval  19676  rgspnval  20525  lspfval  20904  sraval  21107  irinitoringc  21414  zrhval2  21443  aspval  21808  psrmulfval  21878  psrass1  21899  mvrval  21917  mplmon  21968  mplcoe1  21970  evlslem2  22012  mpfrcl  22018  evlsval  22019  evlsvar  22023  mpfind  22040  mhpfval  22051  psdval  22072  psdmul  22079  coe1fval  22116  psropprmul  22148  coe1mul2  22181  ply1coe  22211  evls1fval  22232  evls1val  22233  evl1fval  22241  evl1val  22242  submafval  22492  mdetfval  22499  madufval  22550  minmar1fval  22559  pmatcollpw2lem  22690  pm2mpval  22708  1stcfb  23358  ptbasfi  23494  dfac14  23531  fmval  23856  fmf  23858  flffval  23902  fcfval  23946  cnextval  23974  met1stc  24434  pcoval  24936  iscmet3lem3  25215  rrxsca  25321  mbflimsup  25592  mbflim  25594  itg1climres  25640  mbfi1fseqlem2  25642  mbfi1fseqlem4  25644  mbfi1fseqlem6  25646  mbfi1flimlem  25648  mbfmullem2  25650  itg2monolem1  25676  itg2addlem  25684  itg2cnlem1  25687  cpnfval  25859  mdegfval  25992  elply  26125  plyeq0lem  26140  plypf1  26142  geolim3  26272  ulmuni  26326  ulmcau  26329  ulmdvlem1  26334  ulmdvlem3  26336  mbfulm  26340  itgulm  26342  pserval  26344  dvradcnv  26355  pserdvlem2  26363  abelthlem1  26366  abelthlem3  26368  abelthlem6  26371  logtayl  26594  leibpi  26877  dfef2  26906  emcllem4  26934  emcllem6  26936  emcllem7  26937  lgamgulmlem5  26968  lgamgulmlem6  26969  lgamcvg2  26990  basellem6  27021  sqff1o  27117  dchrptlem2  27201  dchrptlem3  27202  2lgslem1  27330  dchrisumlem3  27427  padicfval  27552  padicabvf  27567  istrkg2ld  28436  mirval  28631  ishpg  28735  lmif  28761  islmib  28763  axlowdim  28937  crctcshlem3  29795  nmoofval  30737  pjhfval  31371  pjmfn  31690  hosmval  31710  hommval  31711  hodmval  31712  hfsmval  31713  hfmmval  31714  eigvalfval  31872  brafval  31918  kbfval  31927  rnbra  32082  bra11  32083  padct  32696  fpwrelmap  32711  qusima  33368  nsgmgc  33372  nsgqusf1o  33376  idlsrgtset  33468  mplvrpmga  33570  esplyval  33580  locfinreflem  33848  rspectopn  33875  zarcmplem  33889  ordtconnlem1  33932  xrhval  34026  sigapildsys  34170  sxbrsigalem2  34294  eulerpart  34390  dstfrvclim1  34486  ballotlemfval  34498  ballotlemsval  34517  signstfv  34571  vtsval  34645  fineqvnttrclse  35132  cvmliftlem5  35321  mrsubffval  35539  mrsubfval  35540  msubffval  35555  msubfval  35556  msubrn  35561  msubco  35563  msubvrs  35592  circum  35706  divcnvlin  35765  climlec3  35766  faclimlem2  35776  faclim2  35780  knoppcnlem1  36526  knoppcnlem6  36531  knoppcnlem7  36532  cnndvlem2  36571  bj-endval  37348  ptrest  37658  poimirlem17  37676  poimirlem20  37679  voliunnfl  37703  volsupnfl  37704  upixp  37768  sdclem2  37781  fdc  37784  lmclim2  37797  geomcau  37798  rrncmslem  37871  pclfvalN  39927  polfvalN  39942  trlset  40199  tendopl  40814  docafvalN  41160  dibfval  41179  dibopelvalN  41181  dibopelval2  41183  dibelval3  41185  dibn0  41191  dib0  41202  diblsmopel  41209  dicn0  41230  dihopelvalcpre  41286  dihatlat  41372  dihpN  41374  dochfval  41388  lcfrlem9  41588  hvmapfval  41797  hvmapval  41798  hdmap1fval  41834  hlhilset  41972  sticksstones10  42187  sticksstones12a  42189  aks6d1c6isolem2  42207  evlsvvvallem2  42594  evlsvvval  42595  selvvvval  42617  evlselv  42619  prjcrvfval  42663  mzpincl  42766  dfac11  43094  dfac21  43098  hbtlem1  43155  hbtlem7  43157  fsovd  44040  mnringmulrcld  44260  dvgrat  44344  radcnvrat  44346  hashnzfzclim  44354  uzmptshftfval  44378  dvradcnv2  44379  binomcxplemrat  44382  binomcxplemcvg  44386  binomcxplemdvsum  44387  binomcxplemnotnn0  44388  addrval  44497  subrval  44498  mulvval  44499  fmuldfeqlem1  45621  fmuldfeq  45622  clim1fr1  45640  climexp  45644  climneg  45649  climdivf  45651  divcnvg  45666  expfac  45694  climresmpt  45696  climsubmpt  45697  limsupval4  45831  climliminflimsupd  45838  liminfreuzlem  45839  liminfltlem  45841  liminfpnfuz  45853  dvsinax  45950  dvcosax  45963  ioodvbdlimc1lem2  45969  ioodvbdlimc2lem  45971  dvnprodlem1  45983  dvnprodlem2  45984  dvnprodlem3  45985  stoweidlem59  46096  wallispilem5  46106  wallispi  46107  stirlinglem1  46111  stirlinglem8  46118  stirlinglem14  46124  stirlinglem15  46125  dirkerval  46128  fourierdlem71  46214  fourierdlem103  46246  fourierdlem104  46247  fourierdlem112  46255  etransclem48  46319  salgensscntex  46381  sge0tsms  46417  nnfoctbdjlem  46492  isomenndlem  46567  ovnval  46578  ovncvrrp  46601  ovnsubaddlem1  46607  hsphoif  46613  hsphoival  46616  ovnhoilem2  46639  hoidifhspval  46645  ovncvr2  46648  hspmbllem2  46664  vonioolem1  46717  smfpimcclem  46844  smflimsuplem1  46857  smflimsuplem4  46860  smflimsuplem7  46863  smfliminflem  46867  fsupdm  46879  smfsupdmmbllem  46881  finfdm  46883  smfinfdmmbllem  46885  cfsetsnfsetfo  47090  isuspgrim0  47924  cycldlenngric  47958  isgrtri  47973  1aryenef  48676  2aryenef  48687  itcovalpclem2  48702  itcovalt2lem2  48707  ackvalsuc1mpt  48709  ackval0  48711  cofidvala  49147  cofidval  49150  isnatd  49254  swapfelvv  49294  swapf2fvala  49295  swapf1vala  49297  swapf2fn  49299  swapf2vala  49301  tposcurf1  49330  prcofelvv  49411  reldmprcof1  49412  reldmprcof2  49413  prcof1  49419  prcof2a  49420  prcof2  49421  idfudiag1bas  49555  idfudiag1  49556  lmdfval  49680  cmdfval  49681  aacllem  49832