Theorem mptex 6124

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 6123	. 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 1802   _Vcvv 3093   |-> cmpt 4491

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-9 1806  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419  ax-rep 4544  ax-sep 4554  ax-nul 4562  ax-pr 4672

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 974  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-eu 2270  df-mo 2271  df-clab 2427  df-cleq 2433  df-clel 2436  df-nfc 2591  df-ne 2638  df-ral 2796  df-rex 2797  df-reu 2798  df-rab 2800  df-v 3095  df-sbc 3312  df-csb 3418  df-dif 3461  df-un 3463  df-in 3465  df-ss 3472  df-nul 3768  df-if 3923  df-sn 4011  df-pr 4013  df-op 4017  df-uni 4231  df-iun 4313  df-br 4434  df-opab 4492  df-mpt 4493  df-id 4781  df-xp 4991  df-rel 4992  df-cnv 4993  df-co 4994  df-dm 4995  df-rn 4996  df-res 4997  df-ima 4998  df-iota 5537  df-fun 5576  df-fn 5577  df-f 5578  df-f1 5579  df-fo 5580  df-f1o 5581  df-fv 5582

This theorem is referenced by:  mptrabex  6125  eufnfv  6127  fvresex  6754  abrexex  6755  ofmres  6777  noinfep  8074  cantnffval  8078  cnfcomlem  8141  cnfcom3clem  8147  cnfcomlemOLD  8149  cnfcom3clemOLD  8155  fseqenlem1  8403  dfacacn  8519  dfac12lem1  8521  infmap2  8596  ackbij2lem2  8618  ackbij2lem3  8619  fin23lem32  8722  konigthlem  8941  wunex2  9114  wuncval2  9123  rpnnen1lem1  11212  rpnnen1lem3  11214  rpnnen1lem5  11216  mptnn0fsupp  12077  ccatfval  12566  swrdval  12618  swrd00  12619  swrd0  12632  revval  12708  repsundef  12717  climmpt  13368  climle  13436  iserabs  13603  isumshft  13625  supcvg  13641  trireciplem  13647  expcnv  13649  explecnv  13650  geolim  13653  geo2lim  13658  cvgrat  13666  mertenslem2  13668  eftlub  13716  rpnnen2lem1  13820  rpnnen2lem2  13821  1arithlem1  14313  1arith  14317  vdwapval  14363  vdwlem6  14376  vdwlem9  14379  restfn  14694  cidfval  14945  cidffn  14947  idfu2nd  15115  idfu1st  15117  idfucl  15119  fucco  15200  homafval  15225  idafval  15253  prf1  15338  prf2fval  15339  prfcl  15341  prf1st  15342  prf2nd  15343  curf1fval  15362  curf11  15364  curf12  15365  curf1cl  15366  curf2  15367  curfcl  15370  hof2val  15394  yonedalem3a  15412  yonedalem4a  15413  yonedalem4b  15414  yonedalem4c  15415  yonedalem3  15418  yonedainv  15419  lubfval  15477  glbfval  15490  grpinvfval  15957  grplactfval  16005  cntzfval  16227  psgnfval  16394  odfval  16426  sylow1lem2  16488  sylow2blem1  16509  sylow2blem2  16510  sylow3lem1  16516  sylow3lem6  16521  pj1fval  16581  vrgpfval  16653  dprdvalOLD  16905  lspfval  17487  sraval  17690  aspval  17845  asclfval  17851  psrmulfval  17906  psrass1  17928  mvrval  17945  mplmon  17993  mplcoe1  17995  evlslem2  18048  mpfrcl  18055  evlsval  18056  evlsvar  18060  mpfind  18073  coe1fval  18112  psropprmul  18147  coe1mul2  18178  ply1coe  18205  ply1coeOLD  18206  evls1fval  18224  evls1val  18225  evl1fval  18232  evl1val  18233  zrhval2  18413  submafval  18948  mdetfval  18955  madufval  19006  minmar1fval  19015  pmatcollpw2lem  19145  pm2mpval  19163  1stcfb  19812  ptbasfi  19948  dfac14  19985  fmval  20310  fmf  20312  flffval  20356  fcfval  20400  cnextval  20427  met1stc  20890  pcoval  21377  iscmet3lem3  21595  mbflimsup  21939  mbflim  21941  itg1climres  21987  mbfi1fseqlem2  21989  mbfi1fseqlem4  21991  mbfi1fseqlem6  21993  mbfi1flimlem  21995  mbfmullem2  21997  itg2monolem1  22023  itg2addlem  22031  itg2cnlem1  22034  cpnfval  22201  mdegfval  22326  ig1pval  22439  elply  22458  plyeq0lem  22473  plypf1  22475  geolim3  22600  ulmuni  22652  ulmcau  22655  ulmdvlem1  22660  ulmdvlem3  22662  mbfulm  22666  itgulm  22668  pserval  22670  dvradcnv  22681  pserdvlem2  22688  abelthlem1  22691  abelthlem3  22693  abelthlem6  22696  logtayl  22906  leibpi  23138  dfef2  23165  emcllem4  23193  emcllem6  23195  emcllem7  23196  basellem6  23224  sqff1o  23321  dchrptlem2  23405  dchrptlem3  23406  dchrisumlem3  23541  padicfval  23666  padicabvf  23681  istrkg2ld  23723  mirval  23901  ishpg  23993  lmif  24016  islmib  24018  axlowdim  24129  wwlkn  24547  clwwlkn  24632  clwwlknprop  24637  eupatrl  24833  numclwlk1lem2  24962  nmoofval  25542  htthlem  25699  pjhfval  26179  pjmfn  26498  hosmval  26519  hommval  26520  hodmval  26521  hfsmval  26522  hfmmval  26523  eigvalfval  26681  brafval  26727  kbfval  26736  rnbra  26891  bra11  26892  fpwrelmap  27421  sgnsv  27583  locfinreflem  27709  ordtconlem1  27772  xrhval  27862  sxbrsigalem2  28123  eulerpart  28187  dstfrvclim1  28282  ballotlemfval  28294  ballotlemsval  28313  signstfv  28386  lgamgulmlem5  28441  lgamgulmlem6  28442  lgamcvg2  28463  cvmliftlem5  28600  mvrsval  28731  mrsubffval  28733  mrsubfval  28734  msubffval  28749  msubfval  28750  msubrn  28755  msubco  28757  mvhfval  28759  msrfval  28763  msubvrs  28786  circum  28906  divcnvshft  28985  divcnvlin  28986  climlec3  28988  faclimlem2  29137  faclim2  29141  ptrest  30016  voliunnfl  30026  volsupnfl  30027  upixp  30188  sdclem2  30203  fdc  30206  lmclim2  30219  geomcau  30220  rrncmslem  30296  mzpincl  30634  dfac11  30976  dfac21  30980  hbtlem1  31040  hbtlem7  31042  rgspnval  31086  dvgrat  31162  radcnvrat  31164  hashnzfzclim  31196  addrval  31322  subrval  31323  mulvval  31324  fmuldfeqlem1  31500  fmuldfeq  31501  clim1fr1  31511  climexp  31515  climneg  31520  climdivf  31522  divcnvg  31537  dvsinax  31608  dvcosax  31623  ioodvbdlimc1lem2  31629  ioodvbdlimc2lem  31631  stoweidlem59  31726  wallispilem5  31736  wallispi  31737  stirlinglem1  31741  stirlinglem8  31748  stirlinglem14  31754  stirlinglem15  31755  dirkerval  31758  fourierdlem71  31845  fourierdlem103  31877  fourierdlem104  31878  fourierdlem112  31886  lkrfval  34514  pmapfval  35182  pclfvalN  35315  polfvalN  35330  watfvalN  35418  ldilfset  35534  ltrnfset  35543  dilfsetN  35579  trnfsetN  35582  trlfset  35587  trlset  35588  tgrpfset  36172  tendofset  36186  tendopl  36204  tendoi  36222  erngfset  36227  erngfset-rN  36235  dvafset  36432  diaffval  36459  dvhfset  36509  docaffvalN  36550  docafvalN  36551  djaffvalN  36562  dibffval  36569  dibfval  36570  dibopelvalN  36572  dibopelval2  36574  dibelval3  36576  dibn0  36582  dib0  36593  diblsmopel  36600  dicffval  36603  dicn0  36621  dihffval  36659  dihfval  36660  dihopelvalcpre  36677  dihatlat  36763  dihpN  36765  dochffval  36778  dochfval  36779  djhffval  36825  lcfrlem8  36978  lcfrlem9  36979  lcdfval  37017  mapdffval  37055  mapdfval  37056  hvmapffval  37187  hvmapfval  37188  hvmapval  37189  hdmap1ffval  37225  hdmap1fval  37226  hdmapffval  37258  hdmapfval  37259  hgmapffval  37317  hgmapfval  37318  hlhilset  37366