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

Theorem mptex 6143
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
Assertion
Ref Expression
mptex
Distinct variable group:   ,

Proof of Theorem mptex
StepHypRef Expression
1 mptex.1 . 2
2 mptexg 6142 . 2
31, 2ax-mp 5 1
Colors of variables: wff setvar class
Syntax hints:  e.wcel 1818   cvv 3109  e.cmpt 4510
This theorem is referenced by:  mptrabex  6144  eufnfv  6146  fvresex  6773  abrexex  6774  ofmres  6796  noinfep  8097  cantnffval  8101  cnfcomlem  8164  cnfcom3clem  8170  cnfcomlemOLD  8172  cnfcom3clemOLD  8178  fseqenlem1  8426  dfacacn  8542  dfac12lem1  8544  infmap2  8619  ackbij2lem2  8641  ackbij2lem3  8642  fin23lem32  8745  konigthlem  8964  wunex2  9137  wuncval2  9146  rpnnen1lem1  11237  rpnnen1lem3  11239  rpnnen1lem5  11241  mptnn0fsupp  12103  ccatfval  12592  swrdval  12644  swrd00  12645  swrd0  12658  revval  12734  repsundef  12743  climmpt  13394  climle  13462  iserabs  13629  isumshft  13651  supcvg  13667  trireciplem  13673  expcnv  13675  explecnv  13676  geolim  13679  geo2lim  13684  cvgrat  13692  mertenslem2  13694  eftlub  13844  rpnnen2lem1  13948  rpnnen2lem2  13949  1arithlem1  14441  1arith  14445  vdwapval  14491  vdwlem6  14504  vdwlem9  14507  restfn  14822  cidfval  15073  cidffn  15075  idfu2nd  15246  idfu1st  15248  idfucl  15250  fucco  15331  homafval  15356  idafval  15384  prf1  15469  prf2fval  15470  prfcl  15472  prf1st  15473  prf2nd  15474  curf1fval  15493  curf11  15495  curf12  15496  curf1cl  15497  curf2  15498  curfcl  15501  hof2val  15525  yonedalem3a  15543  yonedalem4a  15544  yonedalem4b  15545  yonedalem4c  15546  yonedalem3  15549  yonedainv  15550  lubfval  15608  glbfval  15621  grpinvfval  16088  grplactfval  16136  cntzfval  16358  psgnfval  16525  odfval  16557  sylow1lem2  16619  sylow2blem1  16640  sylow2blem2  16641  sylow3lem1  16647  sylow3lem6  16652  pj1fval  16712  vrgpfval  16784  dprdvalOLD  17036  lspfval  17619  sraval  17822  aspval  17977  asclfval  17983  psrmulfval  18038  psrass1  18060  mvrval  18077  mplmon  18125  mplcoe1  18127  evlslem2  18180  mpfrcl  18187  evlsval  18188  evlsvar  18192  mpfind  18205  coe1fval  18244  psropprmul  18279  coe1mul2  18310  ply1coe  18337  ply1coeOLD  18338  evls1fval  18356  evls1val  18357  evl1fval  18364  evl1val  18365  zrhval2  18546  submafval  19081  mdetfval  19088  madufval  19139  minmar1fval  19148  pmatcollpw2lem  19278  pm2mpval  19296  1stcfb  19946  ptbasfi  20082  dfac14  20119  fmval  20444  fmf  20446  flffval  20490  fcfval  20534  cnextval  20561  met1stc  21024  pcoval  21511  iscmet3lem3  21729  mbflimsup  22073  mbflim  22075  itg1climres  22121  mbfi1fseqlem2  22123  mbfi1fseqlem4  22125  mbfi1fseqlem6  22127  mbfi1flimlem  22129  mbfmullem2  22131  itg2monolem1  22157  itg2addlem  22165  itg2cnlem1  22168  cpnfval  22335  mdegfval  22460  ig1pval  22573  elply  22592  plyeq0lem  22607  plypf1  22609  geolim3  22735  ulmuni  22787  ulmcau  22790  ulmdvlem1  22795  ulmdvlem3  22797  mbfulm  22801  itgulm  22803  pserval  22805  dvradcnv  22816  pserdvlem2  22823  abelthlem1  22826  abelthlem3  22828  abelthlem6  22831  logtayl  23041  leibpi  23273  dfef2  23300  emcllem4  23328  emcllem6  23330  emcllem7  23331  basellem6  23359  sqff1o  23456  dchrptlem2  23540  dchrptlem3  23541  dchrisumlem3  23676  padicfval  23801  padicabvf  23816  istrkg2ld  23858  mirval  24036  ishpg  24128  lmif  24151  islmib  24153  axlowdim  24264  wwlkn  24682  clwwlkn  24767  clwwlknprop  24772  eupatrl  24968  numclwlk1lem2  25097  nmoofval  25677  htthlem  25834  pjhfval  26314  pjmfn  26633  hosmval  26654  hommval  26655  hodmval  26656  hfsmval  26657  hfmmval  26658  eigvalfval  26816  brafval  26862  kbfval  26871  rnbra  27026  bra11  27027  fpwrelmap  27556  sgnsv  27717  locfinreflem  27843  ordtconlem1  27906  xrhval  27996  sxbrsigalem2  28257  eulerpart  28321  dstfrvclim1  28416  ballotlemfval  28428  ballotlemsval  28447  signstfv  28520  lgamgulmlem5  28575  lgamgulmlem6  28576  lgamcvg2  28597  cvmliftlem5  28734  mvrsval  28865  mrsubffval  28867  mrsubfval  28868  msubffval  28883  msubfval  28884  msubrn  28889  msubco  28891  mvhfval  28893  msrfval  28897  msubvrs  28920  circum  29040  divcnvshft  29117  divcnvlin  29118  climlec3  29120  faclimlem2  29169  faclim2  29173  ptrest  30048  voliunnfl  30058  volsupnfl  30059  upixp  30220  sdclem2  30235  fdc  30238  lmclim2  30251  geomcau  30252  rrncmslem  30328  mzpincl  30666  dfac11  31008  dfac21  31012  hbtlem1  31072  hbtlem7  31074  rgspnval  31117  dvgrat  31193  radcnvrat  31195  hashnzfzclim  31227  uzmptshftfval  31251  dvradcnv2  31252  binomcxplemrat  31255  binomcxplemcvg  31259  binomcxplemdvsum  31260  binomcxplemnotnn0  31261  addrval  31375  subrval  31376  mulvval  31377  fmuldfeqlem1  31576  fmuldfeq  31577  clim1fr1  31607  climexp  31611  climneg  31616  climdivf  31618  divcnvg  31633  expfac  31663  dvsinax  31708  dvcosax  31723  ioodvbdlimc1lem2  31729  ioodvbdlimc2lem  31731  dvnprodlem1  31743  dvnprodlem2  31744  dvnprodlem3  31745  stoweidlem59  31841  wallispilem5  31851  wallispi  31852  stirlinglem1  31856  stirlinglem8  31863  stirlinglem14  31869  stirlinglem15  31870  dirkerval  31873  fourierdlem71  31960  fourierdlem103  31992  fourierdlem104  31993  fourierdlem112  32001  etransclem48  32065  irinitoringc  32877  aacllem  33216  lkrfval  34812  pmapfval  35480  pclfvalN  35613  polfvalN  35628  watfvalN  35716  ldilfset  35832  ltrnfset  35841  dilfsetN  35877  trnfsetN  35880  trlfset  35885  trlset  35886  tgrpfset  36470  tendofset  36484  tendopl  36502  tendoi  36520  erngfset  36525  erngfset-rN  36533  dvafset  36730  diaffval  36757  dvhfset  36807  docaffvalN  36848  docafvalN  36849  djaffvalN  36860  dibffval  36867  dibfval  36868  dibopelvalN  36870  dibopelval2  36872  dibelval3  36874  dibn0  36880  dib0  36891  diblsmopel  36898  dicffval  36901  dicn0  36919  dihffval  36957  dihfval  36958  dihopelvalcpre  36975  dihatlat  37061  dihpN  37063  dochffval  37076  dochfval  37077  djhffval  37123  lcfrlem8  37276  lcfrlem9  37277  lcdfval  37315  mapdffval  37353  mapdfval  37354  hvmapffval  37485  hvmapfval  37486  hvmapval  37487  hdmap1ffval  37523  hdmap1fval  37524  hdmapffval  37556  hdmapfval  37557  hgmapffval  37615  hgmapfval  37616  hlhilset  37664
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-9 1822  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-rep 4563  ax-sep 4573  ax-nul 4581  ax-pr 4691
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-eu 2286  df-mo 2287  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-reu 2814  df-rab 2816  df-v 3111  df-sbc 3328  df-csb 3435  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-sn 4030  df-pr 4032  df-op 4036  df-uni 4250  df-iun 4332  df-br 4453  df-opab 4511  df-mpt 4512  df-id 4800  df-xp 5010  df-rel 5011  df-cnv 5012  df-co 5013  df-dm 5014  df-rn 5015  df-res 5016  df-ima 5017  df-iota 5556  df-fun 5595  df-fn 5596  df-f 5597  df-f1 5598  df-fo 5599  df-f1o 5600  df-fv 5601
  Copyright terms: Public domain W3C validator