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

Theorem mptex 5762
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 5761 . 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 1696   _Vcvv 2801    e. cmpt 4093
This theorem is referenced by:  eufnfv  5768  fvresex  5778  abrexex  5779  ofmres  6132  noinfep  7376  cantnffval  7380  cnfcomlem  7418  cnfcom3clem  7424  fseqenlem1  7667  dfacacn  7783  dfac12lem1  7785  infmap2  7860  ackbij2lem2  7882  ackbij2lem3  7883  fin23lem32  7986  konigthlem  8206  wunex2  8376  wuncval2  8385  rpnnen1lem1  10358  rpnnen1lem3  10360  rpnnen1lem5  10362  ccatfval  11444  swrdval  11466  swrd00  11467  revval  11494  climmpt  12061  climle  12129  iserabs  12289  isumshft  12314  supcvg  12330  trireciplem  12336  expcnv  12338  explecnv  12339  geolim  12342  geo2lim  12347  cvgrat  12355  mertenslem2  12357  eftlub  12405  rpnnen2lem1  12509  rpnnen2lem2  12510  odzval  12872  1arithlem1  12986  1arith  12990  vdwapval  13036  vdwlem6  13049  vdwlem9  13052  restfn  13345  cidfval  13594  cidffn  13596  idfu2nd  13767  idfu1st  13769  idfucl  13771  fucco  13852  homafval  13877  idafval  13905  prf1  13990  prf2fval  13991  prfcl  13993  prf1st  13994  prf2nd  13995  curf1fval  14014  curf11  14016  curf12  14017  curf1cl  14018  curf2  14019  curfcl  14022  hof2val  14046  yonedalem3a  14064  yonedalem4a  14065  yonedalem4b  14066  yonedalem4c  14067  yonedalem3  14070  yonedainv  14071  lubfval  14128  glbfval  14133  grpinvfval  14536  grplactfval  14578  cntzfval  14812  odfval  14864  sylow1lem2  14926  sylow2blem1  14947  sylow2blem2  14948  sylow3lem1  14954  sylow3lem6  14959  pj1fval  15019  vrgpfval  15091  dmdprd  15252  dprdval  15254  lspfval  15746  sraval  15945  aspval  16084  asclfval  16090  psrmulfval  16146  mvrval  16182  evlslem2  16265  coe1fval  16302  psropprmul  16332  ply1coe  16384  zrhval2  16479  1stcfb  17187  ptbasfi  17292  dfac14  17328  fmval  17654  fmf  17656  flffval  17700  fcfval  17744  met1stc  18083  pcoval  18525  iscmet3lem3  18732  mbflimsup  19037  mbflim  19039  itg1climres  19085  mbfi1fseqlem2  19087  mbfi1fseqlem4  19089  mbfi1fseqlem6  19091  mbfi1flimlem  19093  mbfmullem2  19095  itg2monolem1  19121  itg2addlem  19129  itg2cnlem1  19132  cpnfval  19297  mpfrcl  19418  evlsval  19419  evlsvar  19423  evl1fval  19426  evl1val  19427  mpfind  19444  mdegfval  19464  ig1pval  19574  elply  19593  plyeq0lem  19608  plypf1  19610  geolim3  19735  ulmcau  19788  ulmdvlem1  19793  ulmdvlem3  19795  mbfulm  19798  itgulm  19800  pserval  19802  dvradcnv  19813  pserdvlem2  19820  abelthlem1  19823  abelthlem3  19825  abelthlem6  19828  logtayl  20023  leibpi  20254  dfef2  20281  emcllem4  20308  emcllem6  20310  emcllem7  20311  basellem6  20339  sqff1o  20436  dchrptlem2  20520  dchrptlem3  20521  dchrisumlem3  20656  padicfval  20781  padicabvf  20796  nmoofval  21356  htthlem  21513  pjhfval  21991  pjmfn  22310  hosmval  22331  hommval  22332  hodmval  22333  hfsmval  22334  hfmmval  22335  eigvalfval  22493  brafval  22539  kbfval  22548  rnbra  22703  bra11  22704  ballotlemfval  23064  ballotlemsval  23083  cvmliftlem5  23835  circum  24022  faclimlem5  24121  axlowdim  24661  isaddrv  25749  isnullcv  25755  isucv  25780  ismulcv  25784  cinvlem1  25931  domcatfun  26028  domcatval  26033  codcatfun  26037  codcatval  26039  pfsubkl  26150  pgapspf  26155  pgapspf2  26156  isside0  26267  upixp  26506  sdclem2  26555  fdc  26558  lmclim2  26577  geomcau  26578  rrncmslem  26659  mzpincl  26915  dfac11  27263  dfac21  27267  hbtlem1  27430  hbtlem7  27432  rgspnval  27476  pmtrfval  27496  psgnfval  27526  mdetfval  27590  addrval  27774  subrval  27775  mulvval  27776  fmuldfeq  27816  clim1fr1  27830  climexp  27834  climneg  27839  climdivf  27841  wallispilem5  27921  wallispi  27922  stirlinglem1  27926  stirlinglem8  27933  stirlinglem14  27939  stirlinglem15  27940  lkrfval  29899  pmapfval  30567  pclfvalN  30700  polfvalN  30715  watfvalN  30803  ldilfset  30919  ltrnfset  30928  dilfsetN  30963  trnfsetN  30966  trlfset  30971  trlset  30972  tgrpfset  31555  tendofset  31569  tendopl  31587  tendoi  31605  erngfset  31610  erngfset-rN  31618  dvafset  31815  diaffval  31842  diafval  31843  dvhfset  31892  docaffvalN  31933  docafvalN  31934  djaffvalN  31945  dibffval  31952  dibfval  31953  dibopelvalN  31955  dibopelval2  31957  dibelval3  31959  dibn0  31965  dib0  31976  diblsmopel  31983  dicffval  31986  dicfval  31987  dicn0  32004  dihffval  32042  dihfval  32043  dihopelvalcpre  32060  dihatlat  32146  dihpN  32148  dochffval  32161  dochfval  32162  djhffval  32208  lcfrlem8  32361  lcfrlem9  32362  lcdfval  32400  mapdffval  32438  mapdfval  32439  hvmapffval  32570  hvmapfval  32571  hvmapval  32572  hdmap1ffval  32608  hdmap1fval  32609  hdmapffval  32641  hdmapfval  32642  hgmapffval  32700  hgmapfval  32701  hlhilset  32749
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-14 1700  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277  ax-rep 4147  ax-sep 4157  ax-nul 4165  ax-pr 4230
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-eu 2160  df-mo 2161  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ne 2461  df-ral 2561  df-rex 2562  df-reu 2563  df-rab 2565  df-v 2803  df-sbc 3005  df-csb 3095  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-nul 3469  df-if 3579  df-sn 3659  df-pr 3660  df-op 3662  df-uni 3844  df-iun 3923  df-br 4040  df-opab 4094  df-mpt 4095  df-id 4325  df-xp 4711  df-rel 4712  df-cnv 4713  df-co 4714  df-dm 4715  df-rn 4716  df-res 4717  df-ima 4718  df-iota 5235  df-fun 5273  df-fn 5274  df-f 5275  df-f1 5276  df-fo 5277  df-f1o 5278  df-fv 5279
  Copyright terms: Public domain W3C validator