Theorem mptex 5943

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 5942	. 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 1756   _Vcvv 2967   e. cmpt 4345

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419  ax-rep 4398  ax-sep 4408  ax-nul 4416  ax-pr 4526

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2256  df-mo 2257  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-ral 2715  df-rex 2716  df-reu 2717  df-rab 2719  df-v 2969  df-sbc 3182  df-csb 3284  df-dif 3326  df-un 3328  df-in 3330  df-ss 3337  df-nul 3633  df-if 3787  df-sn 3873  df-pr 3875  df-op 3879  df-uni 4087  df-iun 4168  df-br 4288  df-opab 4346  df-mpt 4347  df-id 4631  df-xp 4841  df-rel 4842  df-cnv 4843  df-co 4844  df-dm 4845  df-rn 4846  df-res 4847  df-ima 4848  df-iota 5376  df-fun 5415  df-fn 5416  df-f 5417  df-f1 5418  df-fo 5419  df-f1o 5420  df-fv 5421

This theorem is referenced by:  mptrabex  5944  eufnfv  5946  fvresex  6545  abrexex  6546  ofmres  6568  noinfep  7857  cantnffval  7861  cnfcomlem  7924  cnfcom3clem  7930  cnfcomlemOLD  7932  cnfcom3clemOLD  7938  fseqenlem1  8186  dfacacn  8302  dfac12lem1  8304  infmap2  8379  ackbij2lem2  8401  ackbij2lem3  8402  fin23lem32  8505  konigthlem  8724  wunex2  8897  wuncval2  8906  rpnnen1lem1  10971  rpnnen1lem3  10973  rpnnen1lem5  10975  ccatfval  12265  swrdval  12305  swrd00  12306  swrd0  12319  revval  12392  repsundef  12401  climmpt  13041  climle  13109  iserabs  13270  isumshft  13294  supcvg  13310  trireciplem  13316  expcnv  13318  explecnv  13319  geolim  13322  geo2lim  13327  cvgrat  13335  mertenslem2  13337  eftlub  13385  rpnnen2lem1  13489  rpnnen2lem2  13490  odzval  13855  1arithlem1  13976  1arith  13980  vdwapval  14026  vdwlem6  14039  vdwlem9  14042  restfn  14355  cidfval  14606  cidffn  14608  idfu2nd  14779  idfu1st  14781  idfucl  14783  fucco  14864  homafval  14889  idafval  14917  prf1  15002  prf2fval  15003  prfcl  15005  prf1st  15006  prf2nd  15007  curf1fval  15026  curf11  15028  curf12  15029  curf1cl  15030  curf2  15031  curfcl  15034  hof2val  15058  yonedalem3a  15076  yonedalem4a  15077  yonedalem4b  15078  yonedalem4c  15079  yonedalem3  15082  yonedainv  15083  lubfval  15140  glbfval  15153  grpinvfval  15567  grplactfval  15613  cntzfval  15829  pmtrfval  15947  psgnfval  15997  odfval  16027  sylow1lem2  16089  sylow2blem1  16110  sylow2blem2  16111  sylow3lem1  16117  sylow3lem6  16122  pj1fval  16182  vrgpfval  16254  dmdprd  16470  dprdval  16475  dprdvalOLD  16477  lspfval  17034  sraval  17237  aspval  17379  asclfval  17385  psrmulfval  17436  psrass1  17458  mvrval  17474  mplmon  17522  mplcoe1  17524  evlslem2  17577  mpfrcl  17584  evlsval  17585  evlsvar  17589  mpfind  17602  coe1fval  17641  psropprmul  17673  coe1mul2  17703  ply1coe  17726  ply1coeOLD  17727  evls1val  17735  evl1fval  17742  evl1val  17743  zrhval2  17920  submafval  18370  mdetfval  18377  madufval  18423  minmar1fval  18432  1stcfb  19029  ptbasfi  19134  dfac14  19171  fmval  19496  fmf  19498  flffval  19542  fcfval  19586  cnextval  19613  met1stc  20076  pcoval  20563  iscmet3lem3  20781  mbflimsup  21124  mbflim  21126  itg1climres  21172  mbfi1fseqlem2  21174  mbfi1fseqlem4  21176  mbfi1fseqlem6  21178  mbfi1flimlem  21180  mbfmullem2  21182  itg2monolem1  21208  itg2addlem  21216  itg2cnlem1  21219  cpnfval  21386  mdegfval  21511  ig1pval  21624  elply  21643  plyeq0lem  21658  plypf1  21660  geolim3  21785  ulmuni  21837  ulmcau  21840  ulmdvlem1  21845  ulmdvlem3  21847  mbfulm  21851  itgulm  21853  pserval  21855  dvradcnv  21866  pserdvlem2  21873  abelthlem1  21876  abelthlem3  21878  abelthlem6  21881  logtayl  22085  leibpi  22317  dfef2  22344  emcllem4  22372  emcllem6  22374  emcllem7  22375  basellem6  22403  sqff1o  22500  dchrptlem2  22584  dchrptlem3  22585  dchrisumlem3  22720  padicfval  22845  padicabvf  22860  mirval  23039  axlowdim  23175  eupatrl  23557  nmoofval  24130  htthlem  24287  pjhfval  24767  pjmfn  25086  hosmval  25107  hommval  25108  hodmval  25109  hfsmval  25110  hfmmval  25111  eigvalfval  25269  brafval  25315  kbfval  25324  rnbra  25479  bra11  25480  fpwrelmap  26001  sgnsv  26158  ordtconlem1  26323  xrhval  26413  sxbrsigalem2  26670  sitgval  26687  eulerpart  26734  dstfrvclim1  26829  ballotlemfval  26841  ballotlemsval  26860  signstfv  26933  lgamgulmlem5  26988  lgamgulmlem6  26989  lgamcvg2  27010  cvmliftlem5  27147  circum  27288  divcnvshft  27367  divcnvlin  27368  climlec3  27370  faclimlem2  27519  faclim2  27523  ptrest  28396  voliunnfl  28406  volsupnfl  28407  upixp  28594  sdclem2  28609  fdc  28612  lmclim2  28625  geomcau  28626  rrncmslem  28702  mzpincl  29041  dfac11  29386  dfac21  29390  hbtlem1  29450  hbtlem7  29452  rgspnval  29496  addrval  29693  subrval  29694  mulvval  29695  fmuldfeqlem1  29734  fmuldfeq  29735  clim1fr1  29745  climexp  29749  climneg  29754  climdivf  29756  stoweidlem59  29825  wallispilem5  29835  wallispi  29836  stirlinglem1  29840  stirlinglem8  29847  stirlinglem14  29853  stirlinglem15  29854  wwlkn  30287  wlknwwlknbij2  30317  wlkiswwlkbij2  30324  wlknwwlknvbij  30343  clwwlkn  30401  clwwlknprop  30406  clwwlkbij  30432  clwwlkvbij  30434  numclwlk1lem2  30661  mptnn0fsupp  30771  pmatcollpw1lem4  30859  pmatcollpw2lem  30862  lkrfval  32625  pmapfval  33293  pclfvalN  33426  polfvalN  33441  watfvalN  33529  ldilfset  33645  ltrnfset  33654  dilfsetN  33689  trnfsetN  33692  trlfset  33697  trlset  33698  tgrpfset  34281  tendofset  34295  tendopl  34313  tendoi  34331  erngfset  34336  erngfset-rN  34344  dvafset  34541  diaffval  34568  diafval  34569  dvhfset  34618  docaffvalN  34659  docafvalN  34660  djaffvalN  34671  dibffval  34678  dibfval  34679  dibopelvalN  34681  dibopelval2  34683  dibelval3  34685  dibn0  34691  dib0  34702  diblsmopel  34709  dicffval  34712  dicfval  34713  dicn0  34730  dihffval  34768  dihfval  34769  dihopelvalcpre  34786  dihatlat  34872  dihpN  34874  dochffval  34887  dochfval  34888  djhffval  34934  lcfrlem8  35087  lcfrlem9  35088  lcdfval  35126  mapdffval  35164  mapdfval  35165  hvmapffval  35296  hvmapfval  35297  hvmapval  35298  hdmap1ffval  35334  hdmap1fval  35335  hdmapffval  35367  hdmapfval  35368  hgmapffval  35426  hgmapfval  35427  hlhilset  35475