Theorem mptex 5925

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 5924	. 2 |- ( A e. _V -> ( x e. A |-> B ) e. _V )
3	1, 2	ax-mp 8	1 |- ( x e. A |-> B ) e. _V

Syntax hints:   e. wcel 1721   _Vcvv 2916   e. cmpt 4226

This theorem is referenced by:  eufnfv  5931  fvresex  5941  abrexex  5942  ofmres  6302  noinfep  7570  cantnffval  7574  cnfcomlem  7612  cnfcom3clem  7618  fseqenlem1  7861  dfacacn  7977  dfac12lem1  7979  infmap2  8054  ackbij2lem2  8076  ackbij2lem3  8077  fin23lem32  8180  konigthlem  8399  wunex2  8569  wuncval2  8578  rpnnen1lem1  10556  rpnnen1lem3  10558  rpnnen1lem5  10560  ccatfval  11697  swrdval  11719  swrd00  11720  revval  11747  climmpt  12320  climle  12388  iserabs  12549  isumshft  12574  supcvg  12590  trireciplem  12596  expcnv  12598  explecnv  12599  geolim  12602  geo2lim  12607  cvgrat  12615  mertenslem2  12617  eftlub  12665  rpnnen2lem1  12769  rpnnen2lem2  12770  odzval  13132  1arithlem1  13246  1arith  13250  vdwapval  13296  vdwlem6  13309  vdwlem9  13312  restfn  13607  cidfval  13856  cidffn  13858  idfu2nd  14029  idfu1st  14031  idfucl  14033  fucco  14114  homafval  14139  idafval  14167  prf1  14252  prf2fval  14253  prfcl  14255  prf1st  14256  prf2nd  14257  curf1fval  14276  curf11  14278  curf12  14279  curf1cl  14280  curf2  14281  curfcl  14284  hof2val  14308  yonedalem3a  14326  yonedalem4a  14327  yonedalem4b  14328  yonedalem4c  14329  yonedalem3  14332  yonedainv  14333  lubfval  14390  glbfval  14395  grpinvfval  14798  grplactfval  14840  cntzfval  15074  odfval  15126  sylow1lem2  15188  sylow2blem1  15209  sylow2blem2  15210  sylow3lem1  15216  sylow3lem6  15221  pj1fval  15281  vrgpfval  15353  dmdprd  15514  dprdval  15516  lspfval  16004  sraval  16203  aspval  16342  asclfval  16348  psrmulfval  16404  mvrval  16440  evlslem2  16523  coe1fval  16558  psropprmul  16587  ply1coe  16639  zrhval2  16745  1stcfb  17461  ptbasfi  17566  dfac14  17603  fmval  17928  fmf  17930  flffval  17974  fcfval  18018  cnextval  18045  met1stc  18504  pcoval  18989  iscmet3lem3  19196  mbflimsup  19511  mbflim  19513  itg1climres  19559  mbfi1fseqlem2  19561  mbfi1fseqlem4  19563  mbfi1fseqlem6  19565  mbfi1flimlem  19567  mbfmullem2  19569  itg2monolem1  19595  itg2addlem  19603  itg2cnlem1  19606  cpnfval  19771  mpfrcl  19892  evlsval  19893  evlsvar  19897  evl1fval  19900  evl1val  19901  mpfind  19918  mdegfval  19938  ig1pval  20048  elply  20067  plyeq0lem  20082  plypf1  20084  geolim3  20209  ulmuni  20261  ulmcau  20264  ulmdvlem1  20269  ulmdvlem3  20271  mbfulm  20275  itgulm  20277  pserval  20279  dvradcnv  20290  pserdvlem2  20297  abelthlem1  20300  abelthlem3  20302  abelthlem6  20305  logtayl  20504  leibpi  20735  dfef2  20762  emcllem4  20790  emcllem6  20792  emcllem7  20793  basellem6  20821  sqff1o  20918  dchrptlem2  21002  dchrptlem3  21003  dchrisumlem3  21138  padicfval  21263  padicabvf  21278  eupatrl  21643  nmoofval  22216  htthlem  22373  pjhfval  22851  pjmfn  23170  hosmval  23191  hommval  23192  hodmval  23193  hfsmval  23194  hfmmval  23195  eigvalfval  23353  brafval  23399  kbfval  23408  rnbra  23563  bra11  23564  xrhval  24337  sxbrsigalem2  24589  sitgval  24600  dstfrvclim1  24688  ballotlemfval  24700  ballotlemsval  24719  lgamgulmlem5  24770  lgamgulmlem6  24771  lgamcvg2  24792  cvmliftlem5  24929  circum  25064  divcnvshft  25164  divcnvlin  25165  climlec3  25167  faclimlem2  25311  faclim2  25315  axlowdim  25804  voliunnfl  26149  volsupnfl  26150  upixp  26321  sdclem2  26336  fdc  26339  lmclim2  26354  geomcau  26355  rrncmslem  26431  mzpincl  26681  dfac11  27028  dfac21  27032  hbtlem1  27195  hbtlem7  27197  rgspnval  27241  pmtrfval  27261  psgnfval  27291  mdetfval  27355  addrval  27538  subrval  27539  mulvval  27540  fmuldfeqlem1  27579  fmuldfeq  27580  clim1fr1  27594  climexp  27598  climneg  27603  climdivf  27605  stoweidlem59  27675  wallispilem5  27685  wallispi  27686  stirlinglem1  27690  stirlinglem8  27697  stirlinglem14  27703  stirlinglem15  27704  lkrfval  29570  pmapfval  30238  pclfvalN  30371  polfvalN  30386  watfvalN  30474  ldilfset  30590  ltrnfset  30599  dilfsetN  30634  trnfsetN  30637  trlfset  30642  trlset  30643  tgrpfset  31226  tendofset  31240  tendopl  31258  tendoi  31276  erngfset  31281  erngfset-rN  31289  dvafset  31486  diaffval  31513  diafval  31514  dvhfset  31563  docaffvalN  31604  docafvalN  31605  djaffvalN  31616  dibffval  31623  dibfval  31624  dibopelvalN  31626  dibopelval2  31628  dibelval3  31630  dibn0  31636  dib0  31647  diblsmopel  31654  dicffval  31657  dicfval  31658  dicn0  31675  dihffval  31713  dihfval  31714  dihopelvalcpre  31731  dihatlat  31817  dihpN  31819  dochffval  31832  dochfval  31833  djhffval  31879  lcfrlem8  32032  lcfrlem9  32033  lcdfval  32071  mapdffval  32109  mapdfval  32110  hvmapffval  32241  hvmapfval  32242  hvmapval  32243  hdmap1ffval  32279  hdmap1fval  32280  hdmapffval  32312  hdmapfval  32313  hgmapffval  32371  hgmapfval  32372  hlhilset  32420

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-rep 4280  ax-sep 4290  ax-nul 4298  ax-pr 4363

This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2258  df-mo 2259  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-ral 2671  df-rex 2672  df-reu 2673  df-rab 2675  df-v 2918  df-sbc 3122  df-csb 3212  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-nul 3589  df-if 3700  df-sn 3780  df-pr 3781  df-op 3783  df-uni 3976  df-iun 4055  df-br 4173  df-opab 4227  df-mpt 4228  df-id 4458  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-rn 4848  df-res 4849  df-ima 4850  df-iota 5377  df-fun 5415  df-fn 5416  df-f 5417  df-f1 5418  df-fo 5419  df-f1o 5420  df-fv 5421