MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mptex Unicode version

Theorem mptex 5746
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
StepHypRef Expression
1 mptex.1 . 2  |-  A  e. 
_V
2 mptexg 5745 . 2  |-  ( A  e.  _V  ->  (
x  e.  A  |->  B )  e.  _V )
31, 2ax-mp 8 1  |-  ( x  e.  A  |->  B )  e.  _V
Colors of variables: wff set class
Syntax hints:    e. wcel 1684   _Vcvv 2788    e. cmpt 4077
This theorem is referenced by:  eufnfv  5752  fvresex  5762  abrexex  5763  ofmres  6116  noinfep  7360  cantnffval  7364  cnfcomlem  7402  cnfcom3clem  7408  fseqenlem1  7651  dfacacn  7767  dfac12lem1  7769  infmap2  7844  ackbij2lem2  7866  ackbij2lem3  7867  fin23lem32  7970  konigthlem  8190  wunex2  8360  wuncval2  8369  rpnnen1lem1  10342  rpnnen1lem3  10344  rpnnen1lem5  10346  ccatfval  11428  swrdval  11450  swrd00  11451  revval  11478  climmpt  12045  climle  12113  iserabs  12273  isumshft  12298  supcvg  12314  trireciplem  12320  expcnv  12322  explecnv  12323  geolim  12326  geo2lim  12331  cvgrat  12339  mertenslem2  12341  eftlub  12389  rpnnen2lem1  12493  rpnnen2lem2  12494  odzval  12856  1arithlem1  12970  1arith  12974  vdwapval  13020  vdwlem6  13033  vdwlem9  13036  restfn  13329  cidfval  13578  cidffn  13580  idfu2nd  13751  idfu1st  13753  idfucl  13755  fucco  13836  homafval  13861  idafval  13889  prf1  13974  prf2fval  13975  prfcl  13977  prf1st  13978  prf2nd  13979  curf1fval  13998  curf11  14000  curf12  14001  curf1cl  14002  curf2  14003  curfcl  14006  hof2val  14030  yonedalem3a  14048  yonedalem4a  14049  yonedalem4b  14050  yonedalem4c  14051  yonedalem3  14054  yonedainv  14055  lubfval  14112  glbfval  14117  grpinvfval  14520  grplactfval  14562  cntzfval  14796  odfval  14848  sylow1lem2  14910  sylow2blem1  14931  sylow2blem2  14932  sylow3lem1  14938  sylow3lem6  14943  pj1fval  15003  vrgpfval  15075  dmdprd  15236  dprdval  15238  lspfval  15730  sraval  15929  aspval  16068  asclfval  16074  psrmulfval  16130  mvrval  16166  evlslem2  16249  coe1fval  16286  psropprmul  16316  ply1coe  16368  zrhval2  16463  1stcfb  17171  ptbasfi  17276  dfac14  17312  fmval  17638  fmf  17640  flffval  17684  fcfval  17728  met1stc  18067  pcoval  18509  iscmet3lem3  18716  mbflimsup  19021  mbflim  19023  itg1climres  19069  mbfi1fseqlem2  19071  mbfi1fseqlem4  19073  mbfi1fseqlem6  19075  mbfi1flimlem  19077  mbfmullem2  19079  itg2monolem1  19105  itg2addlem  19113  itg2cnlem1  19116  cpnfval  19281  mpfrcl  19402  evlsval  19403  evlsvar  19407  evl1fval  19410  evl1val  19411  mpfind  19428  mdegfval  19448  ig1pval  19558  elply  19577  plyeq0lem  19592  plypf1  19594  geolim3  19719  ulmcau  19772  ulmdvlem1  19777  ulmdvlem3  19779  mbfulm  19782  itgulm  19784  pserval  19786  dvradcnv  19797  pserdvlem2  19804  abelthlem1  19807  abelthlem3  19809  abelthlem6  19812  logtayl  20007  leibpi  20238  dfef2  20265  emcllem4  20292  emcllem6  20294  emcllem7  20295  basellem6  20323  sqff1o  20420  dchrptlem2  20504  dchrptlem3  20505  dchrisumlem3  20640  padicfval  20765  padicabvf  20780  nmoofval  21340  htthlem  21497  pjhfval  21975  pjmfn  22294  hosmval  22315  hommval  22316  hodmval  22317  hfsmval  22318  hfmmval  22319  eigvalfval  22477  brafval  22523  kbfval  22532  rnbra  22687  bra11  22688  ballotlemfval  23048  ballotlemsval  23067  cvmliftlem5  23820  circum  24007  axlowdim  24589  isaddrv  25646  isnullcv  25652  isucv  25677  ismulcv  25681  cinvlem1  25828  domcatfun  25925  domcatval  25930  codcatfun  25934  codcatval  25936  pfsubkl  26047  pgapspf  26052  pgapspf2  26053  isside0  26164  upixp  26403  sdclem2  26452  fdc  26455  lmclim2  26474  geomcau  26475  rrncmslem  26556  mzpincl  26812  dfac11  27160  dfac21  27164  hbtlem1  27327  hbtlem7  27329  rgspnval  27373  pmtrfval  27393  psgnfval  27423  mdetfval  27487  addrval  27671  subrval  27672  mulvval  27673  fmuldfeq  27713  clim1fr1  27727  climexp  27731  climneg  27736  climdivf  27738  wallispilem5  27818  wallispi  27819  stirlinglem1  27823  stirlinglem8  27830  stirlinglem14  27836  stirlinglem15  27837  lkrfval  29277  pmapfval  29945  pclfvalN  30078  polfvalN  30093  watfvalN  30181  ldilfset  30297  ltrnfset  30306  dilfsetN  30341  trnfsetN  30344  trlfset  30349  trlset  30350  tgrpfset  30933  tendofset  30947  tendopl  30965  tendoi  30983  erngfset  30988  erngfset-rN  30996  dvafset  31193  diaffval  31220  diafval  31221  dvhfset  31270  docaffvalN  31311  docafvalN  31312  djaffvalN  31323  dibffval  31330  dibfval  31331  dibopelvalN  31333  dibopelval2  31335  dibelval3  31337  dibn0  31343  dib0  31354  diblsmopel  31361  dicffval  31364  dicfval  31365  dicn0  31382  dihffval  31420  dihfval  31421  dihopelvalcpre  31438  dihatlat  31524  dihpN  31526  dochffval  31539  dochfval  31540  djhffval  31586  lcfrlem8  31739  lcfrlem9  31740  lcdfval  31778  mapdffval  31816  mapdfval  31817  hvmapffval  31948  hvmapfval  31949  hvmapval  31950  hdmap1ffval  31986  hdmap1fval  31987  hdmapffval  32019  hdmapfval  32020  hgmapffval  32078  hgmapfval  32079  hlhilset  32127
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-14 1688  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-rep 4131  ax-sep 4141  ax-nul 4149  ax-pr 4214
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-eu 2147  df-mo 2148  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-ral 2548  df-rex 2549  df-reu 2550  df-rab 2552  df-v 2790  df-sbc 2992  df-csb 3082  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-sn 3646  df-pr 3647  df-op 3649  df-uni 3828  df-iun 3907  df-br 4024  df-opab 4078  df-mpt 4079  df-id 4309  df-xp 4695  df-rel 4696  df-cnv 4697  df-co 4698  df-dm 4699  df-rn 4700  df-res 4701  df-ima 4702  df-iota 5219  df-fun 5257  df-fn 5258  df-f 5259  df-f1 5260  df-fo 5261  df-f1o 5262  df-fv 5263
  Copyright terms: Public domain W3C validator