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

Theorem mptex 6002
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 6001 . 2  |-  ( A  e.  _V  ->  (
x  e.  A  |->  B )  e.  _V )
31, 2ax-mp 5 1  |-  ( x  e.  A  |->  B )  e.  _V
Colors of variables: wff set class
Syntax hints:    e. wcel 1728   _Vcvv 2965    e. cmpt 4297
This theorem is referenced by:  eufnfv  6008  fvresex  6018  abrexex  6019  ofmres  6379  noinfep  7650  cantnffval  7654  cnfcomlem  7692  cnfcom3clem  7698  fseqenlem1  7943  dfacacn  8059  dfac12lem1  8061  infmap2  8136  ackbij2lem2  8158  ackbij2lem3  8159  fin23lem32  8262  konigthlem  8481  wunex2  8651  wuncval2  8660  rpnnen1lem1  10638  rpnnen1lem3  10640  rpnnen1lem5  10642  ccatfval  11780  swrdval  11802  swrd00  11803  revval  11830  climmpt  12403  climle  12471  iserabs  12632  isumshft  12657  supcvg  12673  trireciplem  12679  expcnv  12681  explecnv  12682  geolim  12685  geo2lim  12690  cvgrat  12698  mertenslem2  12700  eftlub  12748  rpnnen2lem1  12852  rpnnen2lem2  12853  odzval  13215  1arithlem1  13329  1arith  13333  vdwapval  13379  vdwlem6  13392  vdwlem9  13395  restfn  13690  cidfval  13939  cidffn  13941  idfu2nd  14112  idfu1st  14114  idfucl  14116  fucco  14197  homafval  14222  idafval  14250  prf1  14335  prf2fval  14336  prfcl  14338  prf1st  14339  prf2nd  14340  curf1fval  14359  curf11  14361  curf12  14362  curf1cl  14363  curf2  14364  curfcl  14367  hof2val  14391  yonedalem3a  14409  yonedalem4a  14410  yonedalem4b  14411  yonedalem4c  14412  yonedalem3  14415  yonedainv  14416  lubfval  14473  glbfval  14478  grpinvfval  14881  grplactfval  14923  cntzfval  15157  odfval  15209  sylow1lem2  15271  sylow2blem1  15292  sylow2blem2  15293  sylow3lem1  15299  sylow3lem6  15304  pj1fval  15364  vrgpfval  15436  dmdprd  15597  dprdval  15599  lspfval  16087  sraval  16286  aspval  16425  asclfval  16431  psrmulfval  16487  mvrval  16523  evlslem2  16606  coe1fval  16641  psropprmul  16670  ply1coe  16722  zrhval2  16828  1stcfb  17546  ptbasfi  17651  dfac14  17688  fmval  18013  fmf  18015  flffval  18059  fcfval  18103  cnextval  18130  met1stc  18589  pcoval  19074  iscmet3lem3  19281  mbflimsup  19594  mbflim  19596  itg1climres  19642  mbfi1fseqlem2  19644  mbfi1fseqlem4  19646  mbfi1fseqlem6  19648  mbfi1flimlem  19650  mbfmullem2  19652  itg2monolem1  19678  itg2addlem  19686  itg2cnlem1  19689  cpnfval  19856  mpfrcl  19977  evlsval  19978  evlsvar  19982  evl1fval  19985  evl1val  19986  mpfind  20003  mdegfval  20023  ig1pval  20133  elply  20152  plyeq0lem  20167  plypf1  20169  geolim3  20294  ulmuni  20346  ulmcau  20349  ulmdvlem1  20354  ulmdvlem3  20356  mbfulm  20360  itgulm  20362  pserval  20364  dvradcnv  20375  pserdvlem2  20382  abelthlem1  20385  abelthlem3  20387  abelthlem6  20390  logtayl  20589  leibpi  20820  dfef2  20847  emcllem4  20875  emcllem6  20877  emcllem7  20878  basellem6  20906  sqff1o  21003  dchrptlem2  21087  dchrptlem3  21088  dchrisumlem3  21223  padicfval  21348  padicabvf  21363  eupatrl  21728  nmoofval  22301  htthlem  22458  pjhfval  22936  pjmfn  23255  hosmval  23276  hommval  23277  hodmval  23278  hfsmval  23279  hfmmval  23280  eigvalfval  23438  brafval  23484  kbfval  23493  rnbra  23648  bra11  23649  xrhval  24419  sxbrsigalem2  24671  sitgval  24682  dstfrvclim1  24770  ballotlemfval  24782  ballotlemsval  24801  lgamgulmlem5  24852  lgamgulmlem6  24853  lgamcvg2  24874  cvmliftlem5  25011  circum  25146  divcnvshft  25246  divcnvlin  25247  climlec3  25249  faclimlem2  25398  faclim2  25402  axlowdim  25935  voliunnfl  26290  volsupnfl  26291  upixp  26473  sdclem2  26488  fdc  26491  lmclim2  26506  geomcau  26507  rrncmslem  26583  mzpincl  26903  dfac11  27249  dfac21  27253  hbtlem1  27416  hbtlem7  27418  rgspnval  27462  pmtrfval  27482  psgnfval  27512  mdetfval  27576  addrval  27759  subrval  27760  mulvval  27761  fmuldfeqlem1  27800  fmuldfeq  27801  clim1fr1  27815  climexp  27819  climneg  27824  climdivf  27826  stoweidlem59  27896  wallispilem5  27906  wallispi  27907  stirlinglem1  27911  stirlinglem8  27918  stirlinglem14  27924  stirlinglem15  27925  wwlkn  28462  lkrfval  30059  pmapfval  30727  pclfvalN  30860  polfvalN  30875  watfvalN  30963  ldilfset  31079  ltrnfset  31088  dilfsetN  31123  trnfsetN  31126  trlfset  31131  trlset  31132  tgrpfset  31715  tendofset  31729  tendopl  31747  tendoi  31765  erngfset  31770  erngfset-rN  31778  dvafset  31975  diaffval  32002  diafval  32003  dvhfset  32052  docaffvalN  32093  docafvalN  32094  djaffvalN  32105  dibffval  32112  dibfval  32113  dibopelvalN  32115  dibopelval2  32117  dibelval3  32119  dibn0  32125  dib0  32136  diblsmopel  32143  dicffval  32146  dicfval  32147  dicn0  32164  dihffval  32202  dihfval  32203  dihopelvalcpre  32220  dihatlat  32306  dihpN  32308  dochffval  32321  dochfval  32322  djhffval  32368  lcfrlem8  32521  lcfrlem9  32522  lcdfval  32560  mapdffval  32598  mapdfval  32599  hvmapffval  32730  hvmapfval  32731  hvmapval  32732  hdmap1ffval  32768  hdmap1fval  32769  hdmapffval  32801  hdmapfval  32802  hgmapffval  32860  hgmapfval  32861  hlhilset  32909
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1628  ax-9 1669  ax-8 1690  ax-14 1732  ax-6 1747  ax-7 1752  ax-11 1764  ax-12 1954  ax-ext 2424  ax-rep 4351  ax-sep 4361  ax-nul 4369  ax-pr 4438
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1661  df-eu 2292  df-mo 2293  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2568  df-ne 2608  df-ral 2717  df-rex 2718  df-reu 2719  df-rab 2721  df-v 2967  df-sbc 3171  df-csb 3271  df-dif 3312  df-un 3314  df-in 3316  df-ss 3323  df-nul 3617  df-if 3768  df-sn 3849  df-pr 3850  df-op 3852  df-uni 4045  df-iun 4124  df-br 4244  df-opab 4298  df-mpt 4299  df-id 4533  df-xp 4919  df-rel 4920  df-cnv 4921  df-co 4922  df-dm 4923  df-rn 4924  df-res 4925  df-ima 4926  df-iota 5453  df-fun 5491  df-fn 5492  df-f 5493  df-f1 5494  df-fo 5495  df-f1o 5496  df-fv 5497
  Copyright terms: Public domain W3C validator