Theorem mptex 6118

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 6117	. 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 1823   _Vcvv 3106   |-> cmpt 4497

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-9 1827  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432  ax-rep 4550  ax-sep 4560  ax-nul 4568  ax-pr 4676

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-eu 2288  df-mo 2289  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2651  df-ral 2809  df-rex 2810  df-reu 2811  df-rab 2813  df-v 3108  df-sbc 3325  df-csb 3421  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3784  df-if 3930  df-sn 4017  df-pr 4019  df-op 4023  df-uni 4236  df-iun 4317  df-br 4440  df-opab 4498  df-mpt 4499  df-id 4784  df-xp 4994  df-rel 4995  df-cnv 4996  df-co 4997  df-dm 4998  df-rn 4999  df-res 5000  df-ima 5001  df-iota 5534  df-fun 5572  df-fn 5573  df-f 5574  df-f1 5575  df-fo 5576  df-f1o 5577  df-fv 5578

This theorem is referenced by:  mptrabex  6119  eufnfv  6121  fvresex  6746  abrexex  6747  ofmres  6769  noinfep  8067  cantnffval  8071  cnfcomlem  8134  cnfcom3clem  8140  cnfcomlemOLD  8142  cnfcom3clemOLD  8148  fseqenlem1  8396  dfacacn  8512  dfac12lem1  8514  infmap2  8589  ackbij2lem2  8611  ackbij2lem3  8612  fin23lem32  8715  konigthlem  8934  wunex2  9105  wuncval2  9114  rpnnen1lem1  11209  rpnnen1lem3  11211  rpnnen1lem5  11213  mptnn0fsupp  12085  ccatfn  12579  ccatfval  12581  swrdval  12633  swrd00  12634  swrd0  12650  revval  12725  repsundef  12734  climmpt  13476  climle  13544  iserabs  13711  isumshft  13733  supcvg  13749  trireciplem  13755  expcnv  13757  explecnv  13758  geolim  13761  geo2lim  13766  cvgrat  13774  mertenslem2  13776  eftlub  13926  rpnnen2lem1  14032  rpnnen2lem2  14033  1arithlem1  14525  1arith  14529  vdwapval  14575  vdwlem6  14588  vdwlem9  14591  restfn  14914  cidfval  15165  cidffn  15167  idfu2nd  15365  idfu1st  15367  idfucl  15369  fucco  15450  homafval  15507  idafval  15535  prf1  15668  prf2fval  15669  prfcl  15671  prf1st  15672  prf2nd  15673  curf1fval  15692  curf11  15694  curf12  15695  curf1cl  15696  curf2  15697  curfcl  15700  hof2val  15724  yonedalem3a  15742  yonedalem4a  15743  yonedalem4b  15744  yonedalem4c  15745  yonedalem3  15748  yonedainv  15749  lubfval  15807  glbfval  15820  grpinvfval  16287  grplactfval  16335  cntzfval  16557  psgnfval  16724  odfval  16756  sylow1lem2  16818  sylow2blem1  16839  sylow2blem2  16840  sylow3lem1  16846  sylow3lem6  16851  pj1fval  16911  vrgpfval  16983  dprdvalOLD  17231  lspfval  17814  sraval  18017  aspval  18172  asclfval  18178  psrmulfval  18233  psrass1  18255  mvrval  18272  mplmon  18320  mplcoe1  18322  evlslem2  18375  mpfrcl  18382  evlsval  18383  evlsvar  18387  mpfind  18400  coe1fval  18439  psropprmul  18474  coe1mul2  18505  ply1coe  18532  ply1coeOLD  18533  evls1fval  18551  evls1val  18552  evl1fval  18559  evl1val  18560  zrhval2  18721  submafval  19248  mdetfval  19255  madufval  19306  minmar1fval  19315  pmatcollpw2lem  19445  pm2mpval  19463  1stcfb  20112  ptbasfi  20248  dfac14  20285  fmval  20610  fmf  20612  flffval  20656  fcfval  20700  cnextval  20727  met1stc  21190  pcoval  21677  iscmet3lem3  21895  mbflimsup  22239  mbflim  22241  itg1climres  22287  mbfi1fseqlem2  22289  mbfi1fseqlem4  22291  mbfi1fseqlem6  22293  mbfi1flimlem  22295  mbfmullem2  22297  itg2monolem1  22323  itg2addlem  22331  itg2cnlem1  22334  cpnfval  22501  mdegfval  22626  ig1pval  22739  elply  22758  plyeq0lem  22773  plypf1  22775  geolim3  22901  ulmuni  22953  ulmcau  22956  ulmdvlem1  22961  ulmdvlem3  22963  mbfulm  22967  itgulm  22969  pserval  22971  dvradcnv  22982  pserdvlem2  22989  abelthlem1  22992  abelthlem3  22994  abelthlem6  22997  logtayl  23209  leibpi  23470  dfef2  23498  emcllem4  23526  emcllem6  23528  emcllem7  23529  basellem6  23557  sqff1o  23654  dchrptlem2  23738  dchrptlem3  23739  dchrisumlem3  23874  padicfval  23999  padicabvf  24014  istrkg2ld  24056  mirval  24237  ishpg  24329  lmif  24352  islmib  24354  axlowdim  24466  wwlkn  24884  clwwlkn  24969  clwwlknprop  24974  eupatrl  25170  numclwlk1lem2  25299  nmoofval  25875  htthlem  26032  pjhfval  26512  pjmfn  26831  hosmval  26852  hommval  26853  hodmval  26854  hfsmval  26855  hfmmval  26856  eigvalfval  27014  brafval  27060  kbfval  27069  rnbra  27224  bra11  27225  padct  27776  fpwrelmap  27787  sgnsv  27951  locfinreflem  28078  ordtconlem1  28141  xrhval  28230  sigapildsys  28388  sxbrsigalem2  28494  eulerpart  28585  dstfrvclim1  28680  ballotlemfval  28692  ballotlemsval  28711  signstfv  28784  lgamgulmlem5  28839  lgamgulmlem6  28840  lgamcvg2  28861  cvmliftlem5  28998  mvrsval  29129  mrsubffval  29131  mrsubfval  29132  msubffval  29147  msubfval  29148  msubrn  29153  msubco  29155  mvhfval  29157  msrfval  29161  msubvrs  29184  circum  29304  divcnvshft  29358  divcnvlin  29359  climlec3  29361  faclimlem2  29410  faclim2  29414  ptrest  30288  voliunnfl  30298  volsupnfl  30299  upixp  30460  sdclem2  30475  fdc  30478  lmclim2  30491  geomcau  30492  rrncmslem  30568  mzpincl  30906  dfac11  31247  dfac21  31251  hbtlem1  31313  hbtlem7  31315  rgspnval  31358  dvgrat  31434  radcnvrat  31436  hashnzfzclim  31468  uzmptshftfval  31492  dvradcnv2  31493  binomcxplemrat  31496  binomcxplemcvg  31500  binomcxplemdvsum  31501  binomcxplemnotnn0  31502  addrval  31616  subrval  31617  mulvval  31618  fmuldfeqlem1  31815  fmuldfeq  31816  clim1fr1  31846  climexp  31850  climneg  31855  climdivf  31857  divcnvg  31872  expfac  31902  dvsinax  31947  dvcosax  31962  ioodvbdlimc1lem2  31968  ioodvbdlimc2lem  31970  dvnprodlem1  31982  dvnprodlem2  31983  dvnprodlem3  31984  stoweidlem59  32080  wallispilem5  32090  wallispi  32091  stirlinglem1  32095  stirlinglem8  32102  stirlinglem14  32108  stirlinglem15  32109  dirkerval  32112  fourierdlem71  32199  fourierdlem103  32231  fourierdlem104  32232  fourierdlem112  32240  etransclem48  32304  irinitoringc  33131  aacllem  33604  lkrfval  35209  pmapfval  35877  pclfvalN  36010  polfvalN  36025  watfvalN  36113  ldilfset  36229  ltrnfset  36238  dilfsetN  36274  trnfsetN  36277  trlfset  36282  trlset  36283  tgrpfset  36867  tendofset  36881  tendopl  36899  tendoi  36917  erngfset  36922  erngfset-rN  36930  dvafset  37127  diaffval  37154  dvhfset  37204  docaffvalN  37245  docafvalN  37246  djaffvalN  37257  dibffval  37264  dibfval  37265  dibopelvalN  37267  dibopelval2  37269  dibelval3  37271  dibn0  37277  dib0  37288  diblsmopel  37295  dicffval  37298  dicn0  37316  dihffval  37354  dihfval  37355  dihopelvalcpre  37372  dihatlat  37458  dihpN  37460  dochffval  37473  dochfval  37474  djhffval  37520  lcfrlem8  37673  lcfrlem9  37674  lcdfval  37712  mapdffval  37750  mapdfval  37751  hvmapffval  37882  hvmapfval  37883  hvmapval  37884  hdmap1ffval  37920  hdmap1fval  37921  hdmapffval  37953  hdmapfval  37954  hgmapffval  38012  hgmapfval  38013  hlhilset  38061