Theorem mptex 6859

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

Syntax hints:   ∈ wcel 2083  Vcvv 3440   ↦ cmpt 5047

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1781  ax-4 1795  ax-5 1892  ax-6 1951  ax-7 1996  ax-8 2085  ax-9 2093  ax-10 2114  ax-11 2128  ax-12 2143  ax-13 2346  ax-ext 2771  ax-rep 5088  ax-sep 5101  ax-nul 5108  ax-pr 5228

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3an 1082  df-tru 1528  df-ex 1766  df-nf 1770  df-sb 2045  df-mo 2578  df-eu 2614  df-clab 2778  df-cleq 2790  df-clel 2865  df-nfc 2937  df-ne 2987  df-ral 3112  df-rex 3113  df-reu 3114  df-rab 3116  df-v 3442  df-sbc 3712  df-csb 3818  df-dif 3868  df-un 3870  df-in 3872  df-ss 3880  df-nul 4218  df-if 4388  df-sn 4479  df-pr 4481  df-op 4485  df-uni 4752  df-iun 4833  df-br 4969  df-opab 5031  df-mpt 5048  df-id 5355  df-xp 5456  df-rel 5457  df-cnv 5458  df-co 5459  df-dm 5460  df-rn 5461  df-res 5462  df-ima 5463  df-iota 6196  df-fun 6234  df-fn 6235  df-f 6236  df-f1 6237  df-fo 6238  df-f1o 6239  df-fv 6240

This theorem is referenced by:  mptrabex  6861  mptfvmpt  6863  eufnfv  6864  fvresex  7524  ofmres  7548  noinfep  8976  cantnffval  8979  cnfcomlem  9015  cnfcom3clem  9021  fseqenlem1  9303  dfacacn  9420  dfac12lem1  9422  infmap2  9493  ackbij2lem2  9515  ackbij2lem3  9516  fin23lem32  9619  konigthlem  9843  wunex2  10013  wuncval2  10022  rpnnen1lem1  12231  rpnnen1lem3  12232  rpnnen1lem5  12234  mptnn0fsupp  13219  ccatfn  13774  ccatfval  13775  swrdval  13845  swrd00  13846  swrd0  13860  revval  13962  repsundef  13973  climmpt  14766  climle  14834  iserabs  15007  isumshft  15031  divcnvshft  15047  supcvg  15048  trireciplem  15054  expcnv  15056  explecnv  15057  geolim  15063  geo2lim  15068  cvgrat  15076  mertenslem2  15078  eftlub  15299  rpnnen2lem1  15404  rpnnen2lem2  15405  1arithlem1  16092  1arith  16096  vdwapval  16142  vdwlem6  16155  vdwlem9  16158  restfn  16531  cidffn  16782  idfu2nd  16980  idfu1st  16982  idfucl  16984  fucco  17065  homafval  17122  prf1  17283  prf2fval  17284  prfcl  17286  prf1st  17287  prf2nd  17288  curf1fval  17307  curf11  17309  curf12  17310  curf1cl  17311  curf2  17312  curfcl  17315  hof2val  17339  yonedalem3a  17357  yonedalem4a  17358  yonedalem4b  17359  yonedalem4c  17360  yonedalem3  17363  yonedainv  17364  lubfval  17421  glbfval  17434  cntzfval  18195  psgnfval  18363  sylow1lem2  18458  sylow2blem1  18479  sylow2blem2  18480  sylow3lem1  18486  sylow3lem6  18491  pj1fval  18551  vrgpfval  18623  lspfval  19439  sraval  19642  aspval  19794  psrmulfval  19857  psrass1  19877  mvrval  19893  mplmon  19935  mplcoe1  19937  evlslem2  19983  mpfrcl  19989  evlsval  19990  evlsvar  19994  mpfind  20007  mhpfval  20019  coe1fval  20060  psropprmul  20093  coe1mul2  20124  ply1coe  20151  evls1fval  20169  evls1val  20170  evl1fval  20177  evl1val  20178  zrhval2  20342  submafval  20876  mdetfval  20883  madufval  20934  minmar1fval  20943  pmatcollpw2lem  21073  pm2mpval  21091  1stcfb  21741  ptbasfi  21877  dfac14  21914  fmval  22239  fmf  22241  flffval  22285  fcfval  22329  cnextval  22357  met1stc  22818  pcoval  23302  iscmet3lem3  23580  rrxsca  23686  mbflimsup  23954  mbflim  23956  itg1climres  24002  mbfi1fseqlem2  24004  mbfi1fseqlem4  24006  mbfi1fseqlem6  24008  mbfi1flimlem  24010  mbfmullem2  24012  itg2monolem1  24038  itg2addlem  24046  itg2cnlem1  24049  cpnfval  24216  mdegfval  24343  elply  24472  plyeq0lem  24487  plypf1  24489  geolim3  24615  ulmuni  24667  ulmcau  24670  ulmdvlem1  24675  ulmdvlem3  24677  mbfulm  24681  itgulm  24683  pserval  24685  dvradcnv  24696  pserdvlem2  24703  abelthlem1  24706  abelthlem3  24708  abelthlem6  24711  logtayl  24928  leibpi  25206  dfef2  25234  emcllem4  25262  emcllem6  25264  emcllem7  25265  lgamgulmlem5  25296  lgamgulmlem6  25297  lgamcvg2  25318  basellem6  25349  sqff1o  25445  dchrptlem2  25527  dchrptlem3  25528  2lgslem1  25656  dchrisumlem3  25753  padicfval  25878  padicabvf  25893  istrkg2ld  25932  mirval  26127  ishpg  26231  lmif  26257  islmib  26259  axlowdim  26434  crctcshlem3  27283  nmoofval  28226  pjhfval  28860  pjmfn  29179  hosmval  29199  hommval  29200  hodmval  29201  hfsmval  29202  hfmmval  29203  eigvalfval  29361  brafval  29407  kbfval  29416  rnbra  29571  bra11  29572  padct  30139  fpwrelmap  30153  locfinreflem  30717  ordtconnlem1  30780  xrhval  30872  sigapildsys  31034  sxbrsigalem2  31157  eulerpart  31253  dstfrvclim1  31348  ballotlemfval  31360  ballotlemsval  31379  signstfv  31446  vtsval  31521  cvmliftlem5  32146  mrsubffval  32364  mrsubfval  32365  msubffval  32380  msubfval  32381  msubrn  32386  msubco  32388  msubvrs  32417  circum  32527  divcnvlin  32574  climlec3  32575  faclimlem2  32586  faclim2  32590  knoppcnlem1  33443  knoppcnlem6  33448  knoppcnlem7  33449  cnndvlem2  33488  ptrest  34443  poimirlem17  34461  poimirlem20  34464  voliunnfl  34488  volsupnfl  34489  upixp  34557  sdclem2  34570  fdc  34573  lmclim2  34586  geomcau  34587  rrncmslem  34663  pclfvalN  36577  polfvalN  36592  trlset  36849  tendopl  37464  docafvalN  37810  dibfval  37829  dibopelvalN  37831  dibopelval2  37833  dibelval3  37835  dibn0  37841  dib0  37852  diblsmopel  37859  dicn0  37880  dihopelvalcpre  37936  dihatlat  38022  dihpN  38024  dochfval  38038  lcfrlem9  38238  hvmapfval  38447  hvmapval  38448  hdmap1fval  38484  hlhilset  38622  mzpincl  38837  dfac11  39168  dfac21  39172  hbtlem1  39229  hbtlem7  39231  rgspnval  39274  fsovd  39860  dvgrat  40203  radcnvrat  40205  hashnzfzclim  40213  uzmptshftfval  40237  dvradcnv2  40238  binomcxplemrat  40241  binomcxplemcvg  40245  binomcxplemdvsum  40246  binomcxplemnotnn0  40247  addrval  40358  subrval  40359  mulvval  40360  fmuldfeqlem1  41426  fmuldfeq  41427  clim1fr1  41445  climexp  41449  climneg  41454  climdivf  41456  divcnvg  41471  expfac  41501  climresmpt  41503  climsubmpt  41504  limsupval4  41638  climliminflimsupd  41645  liminfreuzlem  41646  liminfltlem  41648  liminfpnfuz  41660  dvsinax  41760  dvcosax  41774  ioodvbdlimc1lem2  41780  ioodvbdlimc2lem  41782  dvnprodlem1  41794  dvnprodlem2  41795  dvnprodlem3  41796  stoweidlem59  41908  wallispilem5  41918  wallispi  41919  stirlinglem1  41923  stirlinglem8  41930  stirlinglem14  41936  stirlinglem15  41937  dirkerval  41940  fourierdlem71  42026  fourierdlem103  42058  fourierdlem104  42059  fourierdlem112  42067  etransclem48  42131  salgensscntex  42191  sge0tsms  42226  nnfoctbdjlem  42301  isomenndlem  42376  ovnval  42387  ovncvrrp  42410  ovnsubaddlem1  42416  hsphoif  42422  hsphoival  42425  ovnhoilem2  42448  hoidifhspval  42454  ovncvr2  42457  hspmbllem2  42473  vonioolem1  42526  smfpimcclem  42645  smflimsuplem1  42658  smflimsuplem4  42661  smflimsuplem7  42664  smfliminflem  42668  isomuspgrlem2  43502  irinitoringc  43840  aacllem  44404