Theorem mptex 6122

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

Hypothesis

Ref	Expression
mptex.1	|- A e. _V

Assertion

Ref	Expression
mptex	|- ( x e. A |-> B ) e. _V

Distinct variable group:   x, A

Allowed substitution hint:   B( x)

Proof of Theorem mptex

Step	Hyp	Ref	Expression
1		mptex.1	. 2 |- A e. _V
2		mptexg 6121	. 2 |- ( A e. _V -> ( x e. A |-> B ) e. _V )
3	1, 2	ax-mp 5	1 |- ( x e. A |-> B ) e. _V

Syntax hints:   e. wcel 1762   _Vcvv 3106   |-> cmpt 4498

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-9 1766  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438  ax-rep 4551  ax-sep 4561  ax-nul 4569  ax-pr 4679

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 970  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-eu 2272  df-mo 2273  df-clab 2446  df-cleq 2452  df-clel 2455  df-nfc 2610  df-ne 2657  df-ral 2812  df-rex 2813  df-reu 2814  df-rab 2816  df-v 3108  df-sbc 3325  df-csb 3429  df-dif 3472  df-un 3474  df-in 3476  df-ss 3483  df-nul 3779  df-if 3933  df-sn 4021  df-pr 4023  df-op 4027  df-uni 4239  df-iun 4320  df-br 4441  df-opab 4499  df-mpt 4500  df-id 4788  df-xp 4998  df-rel 4999  df-cnv 5000  df-co 5001  df-dm 5002  df-rn 5003  df-res 5004  df-ima 5005  df-iota 5542  df-fun 5581  df-fn 5582  df-f 5583  df-f1 5584  df-fo 5585  df-f1o 5586  df-fv 5587

This theorem is referenced by:  mptrabex  6123  eufnfv  6125  fvresex  6747  abrexex  6748  ofmres  6770  noinfep  8065  cantnffval  8069  cnfcomlem  8132  cnfcom3clem  8138  cnfcomlemOLD  8140  cnfcom3clemOLD  8146  fseqenlem1  8394  dfacacn  8510  dfac12lem1  8512  infmap2  8587  ackbij2lem2  8609  ackbij2lem3  8610  fin23lem32  8713  konigthlem  8932  wunex2  9105  wuncval2  9114  rpnnen1lem1  11197  rpnnen1lem3  11199  rpnnen1lem5  11201  mptnn0fsupp  12059  ccatfval  12544  swrdval  12594  swrd00  12595  swrd0  12608  revval  12684  repsundef  12693  climmpt  13343  climle  13411  iserabs  13578  isumshft  13603  supcvg  13619  trireciplem  13625  expcnv  13627  explecnv  13628  geolim  13631  geo2lim  13636  cvgrat  13644  mertenslem2  13646  eftlub  13694  rpnnen2lem1  13798  rpnnen2lem2  13799  odzval  14166  1arithlem1  14289  1arith  14293  vdwapval  14339  vdwlem6  14352  vdwlem9  14355  restfn  14669  cidfval  14920  cidffn  14922  idfu2nd  15093  idfu1st  15095  idfucl  15097  fucco  15178  homafval  15203  idafval  15231  prf1  15316  prf2fval  15317  prfcl  15319  prf1st  15320  prf2nd  15321  curf1fval  15340  curf11  15342  curf12  15343  curf1cl  15344  curf2  15345  curfcl  15348  hof2val  15372  yonedalem3a  15390  yonedalem4a  15391  yonedalem4b  15392  yonedalem4c  15393  yonedalem3  15396  yonedainv  15397  lubfval  15454  glbfval  15467  grpinvfval  15882  grplactfval  15930  cntzfval  16146  pmtrfval  16264  psgnfval  16314  odfval  16346  sylow1lem2  16408  sylow2blem1  16429  sylow2blem2  16430  sylow3lem1  16436  sylow3lem6  16441  pj1fval  16501  vrgpfval  16573  dmdprd  16813  dprdval  16818  dprdvalOLD  16820  lspfval  17395  sraval  17598  aspval  17741  asclfval  17747  psrmulfval  17802  psrass1  17824  mvrval  17841  mplmon  17889  mplcoe1  17891  evlslem2  17944  mpfrcl  17951  evlsval  17952  evlsvar  17956  mpfind  17969  coe1fval  18008  psropprmul  18043  coe1mul2  18074  ply1coe  18101  ply1coeOLD  18102  evls1val  18121  evl1fval  18128  evl1val  18129  zrhval2  18306  submafval  18841  mdetfval  18848  madufval  18899  minmar1fval  18908  pmatcollpw2lem  19038  pm2mpval  19056  1stcfb  19705  ptbasfi  19810  dfac14  19847  fmval  20172  fmf  20174  flffval  20218  fcfval  20262  cnextval  20289  met1stc  20752  pcoval  21239  iscmet3lem3  21457  mbflimsup  21801  mbflim  21803  itg1climres  21849  mbfi1fseqlem2  21851  mbfi1fseqlem4  21853  mbfi1fseqlem6  21855  mbfi1flimlem  21857  mbfmullem2  21859  itg2monolem1  21885  itg2addlem  21893  itg2cnlem1  21896  cpnfval  22063  mdegfval  22188  ig1pval  22301  elply  22320  plyeq0lem  22335  plypf1  22337  geolim3  22462  ulmuni  22514  ulmcau  22517  ulmdvlem1  22522  ulmdvlem3  22524  mbfulm  22528  itgulm  22530  pserval  22532  dvradcnv  22543  pserdvlem2  22550  abelthlem1  22553  abelthlem3  22555  abelthlem6  22558  logtayl  22762  leibpi  22994  dfef2  23021  emcllem4  23049  emcllem6  23051  emcllem7  23052  basellem6  23080  sqff1o  23177  dchrptlem2  23261  dchrptlem3  23262  dchrisumlem3  23397  padicfval  23522  padicabvf  23537  istrkg2ld  23579  mirval  23742  lmif  23821  islmib  23823  axlowdim  23933  wwlkn  24344  wlknwwlknbij2  24376  wlkiswwlkbij2  24383  wlknwwlknvbij  24402  clwwlkn  24429  clwwlknprop  24434  clwwlkbij  24461  clwwlkvbij  24463  eupatrl  24630  nmoofval  25203  htthlem  25360  pjhfval  25840  pjmfn  26159  hosmval  26180  hommval  26181  hodmval  26182  hfsmval  26183  hfmmval  26184  eigvalfval  26342  brafval  26388  kbfval  26397  rnbra  26552  bra11  26553  fpwrelmap  27078  sgnsv  27229  ordtconlem1  27392  xrhval  27482  sxbrsigalem2  27747  sitgval  27764  eulerpart  27811  dstfrvclim1  27906  ballotlemfval  27918  ballotlemsval  27937  signstfv  28010  lgamgulmlem5  28065  lgamgulmlem6  28066  lgamcvg2  28087  cvmliftlem5  28224  circum  28365  divcnvshft  28444  divcnvlin  28445  climlec3  28447  faclimlem2  28596  faclim2  28600  ptrest  29476  voliunnfl  29486  volsupnfl  29487  upixp  29674  sdclem2  29689  fdc  29692  lmclim2  29705  geomcau  29706  rrncmslem  29782  mzpincl  30121  dfac11  30465  dfac21  30469  hbtlem1  30529  hbtlem7  30531  rgspnval  30575  addrval  30772  subrval  30773  mulvval  30774  fmuldfeqlem1  30951  fmuldfeq  30952  clim1fr1  30962  climexp  30966  climneg  30971  climdivf  30973  divcnvg  30988  dvsinax  31060  ioodvbdlimc1lem2  31081  ioodvbdlimc2lem  31083  stoweidlem59  31178  wallispilem5  31188  wallispi  31189  stirlinglem1  31193  stirlinglem8  31200  stirlinglem14  31206  stirlinglem15  31207  dirkerval  31210  fourierdlem71  31297  fourierdlem103  31329  fourierdlem104  31330  fourierdlem112  31338  numclwlk1lem2  31816  lkrfval  33759  pmapfval  34427  pclfvalN  34560  polfvalN  34575  watfvalN  34663  ldilfset  34779  ltrnfset  34788  dilfsetN  34823  trnfsetN  34826  trlfset  34831  trlset  34832  tgrpfset  35415  tendofset  35429  tendopl  35447  tendoi  35465  erngfset  35470  erngfset-rN  35478  dvafset  35675  diaffval  35702  diafval  35703  dvhfset  35752  docaffvalN  35793  docafvalN  35794  djaffvalN  35805  dibffval  35812  dibfval  35813  dibopelvalN  35815  dibopelval2  35817  dibelval3  35819  dibn0  35825  dib0  35836  diblsmopel  35843  dicffval  35846  dicfval  35847  dicn0  35864  dihffval  35902  dihfval  35903  dihopelvalcpre  35920  dihatlat  36006  dihpN  36008  dochffval  36021  dochfval  36022  djhffval  36068  lcfrlem8  36221  lcfrlem9  36222  lcdfval  36260  mapdffval  36298  mapdfval  36299  hvmapffval  36430  hvmapfval  36431  hvmapval  36432  hdmap1ffval  36468  hdmap1fval  36469  hdmapffval  36501  hdmapfval  36502  hgmapffval  36560  hgmapfval  36561  hlhilset  36609