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

Theorem mptex 5907
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 5906 . 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 1717   _Vcvv 2901    e. cmpt 4209
This theorem is referenced by:  eufnfv  5913  fvresex  5923  abrexex  5924  ofmres  6284  noinfep  7549  cantnffval  7553  cnfcomlem  7591  cnfcom3clem  7597  fseqenlem1  7840  dfacacn  7956  dfac12lem1  7958  infmap2  8033  ackbij2lem2  8055  ackbij2lem3  8056  fin23lem32  8159  konigthlem  8378  wunex2  8548  wuncval2  8557  rpnnen1lem1  10534  rpnnen1lem3  10536  rpnnen1lem5  10538  ccatfval  11671  swrdval  11693  swrd00  11694  revval  11721  climmpt  12294  climle  12362  iserabs  12523  isumshft  12548  supcvg  12564  trireciplem  12570  expcnv  12572  explecnv  12573  geolim  12576  geo2lim  12581  cvgrat  12589  mertenslem2  12591  eftlub  12639  rpnnen2lem1  12743  rpnnen2lem2  12744  odzval  13106  1arithlem1  13220  1arith  13224  vdwapval  13270  vdwlem6  13283  vdwlem9  13286  restfn  13581  cidfval  13830  cidffn  13832  idfu2nd  14003  idfu1st  14005  idfucl  14007  fucco  14088  homafval  14113  idafval  14141  prf1  14226  prf2fval  14227  prfcl  14229  prf1st  14230  prf2nd  14231  curf1fval  14250  curf11  14252  curf12  14253  curf1cl  14254  curf2  14255  curfcl  14258  hof2val  14282  yonedalem3a  14300  yonedalem4a  14301  yonedalem4b  14302  yonedalem4c  14303  yonedalem3  14306  yonedainv  14307  lubfval  14364  glbfval  14369  grpinvfval  14772  grplactfval  14814  cntzfval  15048  odfval  15100  sylow1lem2  15162  sylow2blem1  15183  sylow2blem2  15184  sylow3lem1  15190  sylow3lem6  15195  pj1fval  15255  vrgpfval  15327  dmdprd  15488  dprdval  15490  lspfval  15978  sraval  16177  aspval  16316  asclfval  16322  psrmulfval  16378  mvrval  16414  evlslem2  16497  coe1fval  16532  psropprmul  16561  ply1coe  16613  zrhval2  16715  1stcfb  17431  ptbasfi  17536  dfac14  17573  fmval  17898  fmf  17900  flffval  17944  fcfval  17988  cnextval  18015  met1stc  18443  pcoval  18909  iscmet3lem3  19116  mbflimsup  19427  mbflim  19429  itg1climres  19475  mbfi1fseqlem2  19477  mbfi1fseqlem4  19479  mbfi1fseqlem6  19481  mbfi1flimlem  19483  mbfmullem2  19485  itg2monolem1  19511  itg2addlem  19519  itg2cnlem1  19522  cpnfval  19687  mpfrcl  19808  evlsval  19809  evlsvar  19813  evl1fval  19816  evl1val  19817  mpfind  19834  mdegfval  19854  ig1pval  19964  elply  19983  plyeq0lem  19998  plypf1  20000  geolim3  20125  ulmuni  20177  ulmcau  20180  ulmdvlem1  20185  ulmdvlem3  20187  mbfulm  20191  itgulm  20193  pserval  20195  dvradcnv  20206  pserdvlem2  20213  abelthlem1  20216  abelthlem3  20218  abelthlem6  20221  logtayl  20420  leibpi  20651  dfef2  20678  emcllem4  20706  emcllem6  20708  emcllem7  20709  basellem6  20737  sqff1o  20834  dchrptlem2  20918  dchrptlem3  20919  dchrisumlem3  21054  padicfval  21179  padicabvf  21194  eupatrl  21540  nmoofval  22113  htthlem  22270  pjhfval  22748  pjmfn  23067  hosmval  23088  hommval  23089  hodmval  23090  hfsmval  23091  hfmmval  23092  eigvalfval  23250  brafval  23296  kbfval  23305  rnbra  23460  bra11  23461  sxbrsigalem2  24432  dstfrvclim1  24516  ballotlemfval  24528  ballotlemsval  24547  lgamgulmlem5  24598  lgamgulmlem6  24599  lgamcvg2  24620  cvmliftlem5  24757  circum  24892  divcnvshft  24992  divcnvlin  24993  climlec3  24995  faclimlem2  25123  faclim2  25127  axlowdim  25616  voliunnfl  25957  volsupnfl  25958  upixp  26124  sdclem2  26139  fdc  26142  lmclim2  26157  geomcau  26158  rrncmslem  26234  mzpincl  26484  dfac11  26831  dfac21  26835  hbtlem1  26998  hbtlem7  27000  rgspnval  27044  pmtrfval  27064  psgnfval  27094  mdetfval  27158  addrval  27341  subrval  27342  mulvval  27343  fmuldfeqlem1  27382  fmuldfeq  27383  clim1fr1  27397  climexp  27401  climneg  27406  climdivf  27408  stoweidlem59  27478  wallispilem5  27488  wallispi  27489  stirlinglem1  27493  stirlinglem8  27500  stirlinglem14  27506  stirlinglem15  27507  lkrfval  29204  pmapfval  29872  pclfvalN  30005  polfvalN  30020  watfvalN  30108  ldilfset  30224  ltrnfset  30233  dilfsetN  30268  trnfsetN  30271  trlfset  30276  trlset  30277  tgrpfset  30860  tendofset  30874  tendopl  30892  tendoi  30910  erngfset  30915  erngfset-rN  30923  dvafset  31120  diaffval  31147  diafval  31148  dvhfset  31197  docaffvalN  31238  docafvalN  31239  djaffvalN  31250  dibffval  31257  dibfval  31258  dibopelvalN  31260  dibopelval2  31262  dibelval3  31264  dibn0  31270  dib0  31281  diblsmopel  31288  dicffval  31291  dicfval  31292  dicn0  31309  dihffval  31347  dihfval  31348  dihopelvalcpre  31365  dihatlat  31451  dihpN  31453  dochffval  31466  dochfval  31467  djhffval  31513  lcfrlem8  31666  lcfrlem9  31667  lcdfval  31705  mapdffval  31743  mapdfval  31744  hvmapffval  31875  hvmapfval  31876  hvmapval  31877  hdmap1ffval  31913  hdmap1fval  31914  hdmapffval  31946  hdmapfval  31947  hgmapffval  32005  hgmapfval  32006  hlhilset  32054
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 1661  ax-8 1682  ax-14 1721  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2370  ax-rep 4263  ax-sep 4273  ax-nul 4281  ax-pr 4346
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 2244  df-mo 2245  df-clab 2376  df-cleq 2382  df-clel 2385  df-nfc 2514  df-ne 2554  df-ral 2656  df-rex 2657  df-reu 2658  df-rab 2660  df-v 2903  df-sbc 3107  df-csb 3197  df-dif 3268  df-un 3270  df-in 3272  df-ss 3279  df-nul 3574  df-if 3685  df-sn 3765  df-pr 3766  df-op 3768  df-uni 3960  df-iun 4039  df-br 4156  df-opab 4210  df-mpt 4211  df-id 4441  df-xp 4826  df-rel 4827  df-cnv 4828  df-co 4829  df-dm 4830  df-rn 4831  df-res 4832  df-ima 4833  df-iota 5360  df-fun 5398  df-fn 5399  df-f 5400  df-f1 5401  df-fo 5402  df-f1o 5403  df-fv 5404
  Copyright terms: Public domain W3C validator