Theorem mptex 6136

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 6135	. 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 1887   _Vcvv 3045   |-> cmpt 4461

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-9 1896  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431  ax-rep 4515  ax-sep 4525  ax-nul 4534  ax-pr 4639

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 987  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-eu 2303  df-mo 2304  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-ne 2624  df-ral 2742  df-rex 2743  df-reu 2744  df-rab 2746  df-v 3047  df-sbc 3268  df-csb 3364  df-dif 3407  df-un 3409  df-in 3411  df-ss 3418  df-nul 3732  df-if 3882  df-sn 3969  df-pr 3971  df-op 3975  df-uni 4199  df-iun 4280  df-br 4403  df-opab 4462  df-mpt 4463  df-id 4749  df-xp 4840  df-rel 4841  df-cnv 4842  df-co 4843  df-dm 4844  df-rn 4845  df-res 4846  df-ima 4847  df-iota 5546  df-fun 5584  df-fn 5585  df-f 5586  df-f1 5587  df-fo 5588  df-f1o 5589  df-fv 5590

This theorem is referenced by:  mptrabex  6137  eufnfv  6139  fvresex  6766  abrexex  6767  ofmres  6789  noinfep  8165  cantnffval  8168  cnfcomlem  8204  cnfcom3clem  8210  fseqenlem1  8455  dfacacn  8571  dfac12lem1  8573  infmap2  8648  ackbij2lem2  8670  ackbij2lem3  8671  fin23lem32  8774  konigthlem  8993  wunex2  9163  wuncval2  9172  rpnnen1lem1  11290  rpnnen1lem3  11292  rpnnen1lem5  11294  mptnn0fsupp  12209  ccatfn  12717  ccatfval  12719  swrdval  12773  swrd00  12774  swrd0  12790  revval  12865  repsundef  12874  climmpt  13635  climle  13703  iserabs  13875  isumshft  13897  divcnvshft  13913  supcvg  13914  trireciplem  13920  expcnv  13922  explecnv  13923  geolim  13926  geo2lim  13931  cvgrat  13939  mertenslem2  13941  eftlub  14163  rpnnen2lem1  14267  rpnnen2lem2  14268  1arithlem1  14867  1arith  14871  vdwapval  14923  vdwlem6  14936  vdwlem9  14939  restfn  15323  cidfval  15582  cidffn  15584  idfu2nd  15782  idfu1st  15784  idfucl  15786  fucco  15867  homafval  15924  idafval  15952  prf1  16085  prf2fval  16086  prfcl  16088  prf1st  16089  prf2nd  16090  curf1fval  16109  curf11  16111  curf12  16112  curf1cl  16113  curf2  16114  curfcl  16117  hof2val  16141  yonedalem3a  16159  yonedalem4a  16160  yonedalem4b  16161  yonedalem4c  16162  yonedalem3  16165  yonedainv  16166  lubfval  16224  glbfval  16237  grpinvfval  16704  grplactfval  16752  cntzfval  16974  psgnfval  17141  odfval  17179  odfvalOLD  17182  sylow1lem2  17251  sylow2blem1  17272  sylow2blem2  17273  sylow3lem1  17279  sylow3lem6  17284  pj1fval  17344  vrgpfval  17416  lspfval  18196  sraval  18399  aspval  18552  asclfval  18558  psrmulfval  18609  psrass1  18629  mvrval  18645  mplmon  18687  mplcoe1  18689  evlslem2  18735  mpfrcl  18741  evlsval  18742  evlsvar  18746  mpfind  18759  coe1fval  18798  psropprmul  18831  coe1mul2  18862  ply1coe  18889  ply1coeOLD  18890  evls1fval  18908  evls1val  18909  evl1fval  18916  evl1val  18917  zrhval2  19080  submafval  19604  mdetfval  19611  madufval  19662  minmar1fval  19671  pmatcollpw2lem  19801  pm2mpval  19819  1stcfb  20460  ptbasfi  20596  dfac14  20633  fmval  20958  fmf  20960  flffval  21004  fcfval  21048  cnextval  21076  met1stc  21536  pcoval  22042  iscmet3lem3  22260  mbflimsup  22623  mbflimsupOLD  22624  mbflim  22626  itg1climres  22672  mbfi1fseqlem2  22674  mbfi1fseqlem4  22676  mbfi1fseqlem6  22678  mbfi1flimlem  22680  mbfmullem2  22682  itg2monolem1  22708  itg2addlem  22716  itg2cnlem1  22719  cpnfval  22886  mdegfval  23011  ig1pval  23124  ig1pvalOLD  23130  elply  23149  plyeq0lem  23164  plypf1  23166  geolim3  23295  ulmuni  23347  ulmcau  23350  ulmdvlem1  23355  ulmdvlem3  23357  mbfulm  23361  itgulm  23363  pserval  23365  dvradcnv  23376  pserdvlem2  23383  abelthlem1  23386  abelthlem3  23388  abelthlem6  23391  logtayl  23605  leibpi  23868  dfef2  23896  emcllem4  23924  emcllem6  23926  emcllem7  23927  lgamgulmlem5  23958  lgamgulmlem6  23959  lgamcvg2  23980  basellem6  24012  sqff1o  24109  dchrptlem2  24193  dchrptlem3  24194  dchrisumlem3  24329  padicfval  24454  padicabvf  24469  istrkg2ld  24508  ishlg  24647  mirval  24700  ishpg  24801  lmif  24827  islmib  24829  axlowdim  24991  wwlkn  25410  clwwlkn  25495  clwwlknprop  25500  eupatrl  25696  numclwlk1lem2  25825  nmoofval  26403  htthlem  26570  pjhfval  27049  pjmfn  27368  hosmval  27388  hommval  27389  hodmval  27390  hfsmval  27391  hfmmval  27392  eigvalfval  27550  brafval  27596  kbfval  27605  rnbra  27760  bra11  27761  padct  28307  fpwrelmap  28318  sgnsv  28490  locfinreflem  28667  ordtconlem1  28730  xrhval  28822  sigapildsys  28984  sxbrsigalem2  29108  eulerpart  29215  dstfrvclim1  29310  ballotlemfval  29322  ballotlemsval  29341  ballotlemsvalOLD  29379  signstfv  29452  cvmliftlem5  30012  mvrsval  30143  mrsubffval  30145  mrsubfval  30146  msubffval  30161  msubfval  30162  msubrn  30167  msubco  30169  mvhfval  30171  msrfval  30175  msubvrs  30198  circum  30318  divcnvlin  30367  climlec3  30369  faclimlem2  30380  faclim2  30384  ptrest  31939  poimirlem17  31957  poimirlem20  31960  voliunnfl  31984  volsupnfl  31985  upixp  32056  sdclem2  32071  fdc  32074  lmclim2  32087  geomcau  32088  rrncmslem  32164  lkrfval  32653  pmapfval  33321  pclfvalN  33454  polfvalN  33469  watfvalN  33557  ldilfset  33673  ltrnfset  33682  dilfsetN  33718  trnfsetN  33721  trlfset  33726  trlset  33727  tgrpfset  34311  tendofset  34325  tendopl  34343  tendoi  34361  erngfset  34366  erngfset-rN  34374  dvafset  34571  diaffval  34598  dvhfset  34648  docaffvalN  34689  docafvalN  34690  djaffvalN  34701  dibffval  34708  dibfval  34709  dibopelvalN  34711  dibopelval2  34713  dibelval3  34715  dibn0  34721  dib0  34732  diblsmopel  34739  dicffval  34742  dicn0  34760  dihffval  34798  dihfval  34799  dihopelvalcpre  34816  dihatlat  34902  dihpN  34904  dochffval  34917  dochfval  34918  djhffval  34964  lcfrlem8  35117  lcfrlem9  35118  lcdfval  35156  mapdffval  35194  mapdfval  35195  hvmapffval  35326  hvmapfval  35327  hvmapval  35328  hdmap1ffval  35364  hdmap1fval  35365  hdmapffval  35397  hdmapfval  35398  hgmapffval  35456  hgmapfval  35457  hlhilset  35505  mzpincl  35576  dfac11  35920  dfac21  35924  hbtlem1  35982  hbtlem7  35984  rgspnval  36034  dvgrat  36661  radcnvrat  36663  hashnzfzclim  36671  uzmptshftfval  36695  dvradcnv2  36696  binomcxplemrat  36699  binomcxplemcvg  36703  binomcxplemdvsum  36704  binomcxplemnotnn0  36705  addrval  36819  subrval  36820  mulvval  36821  fmuldfeqlem1  37660  fmuldfeq  37661  clim1fr1  37679  climexp  37683  climneg  37689  climdivf  37692  divcnvg  37707  expfac  37738  dvsinax  37783  dvcosax  37798  ioodvbdlimc1lem2  37804  ioodvbdlimc1lem2OLD  37806  ioodvbdlimc2lem  37808  ioodvbdlimc2lemOLD  37809  dvnprodlem1  37821  dvnprodlem2  37822  dvnprodlem3  37823  stoweidlem59  37920  wallispilem5  37931  wallispi  37932  stirlinglem1  37936  stirlinglem8  37943  stirlinglem14  37949  stirlinglem15  37950  dirkerval  37953  fourierdlem71  38041  fourierdlem103  38073  fourierdlem104  38074  fourierdlem112  38082  etransclem48OLD  38147  etransclem48  38148  salgensscntex  38203  sge0tsms  38222  nnfoctbdjlem  38293  isomenndlem  38351  ovnval  38362  ovncvrrp  38386  ovnsubaddlem1  38392  hsphoif  38398  hsphoival  38401  ovnhoilem2  38424  hoidifhspval  38430  ovncvr2  38433  hspmbllem2  38449  vtxdushgrfvedglem  39542  vtxdushgrfvedg  39543  irinitoringc  40124  aacllem  40593