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

Theorem mptexg 6142
Description: If the domain of a function given by maps-to notation is a set, the function is a set. (Contributed by FL, 6-Jun-2011.) (Revised by Mario Carneiro, 31-Aug-2015.)
Assertion
Ref Expression
mptexg
Distinct variable group:   ,

Proof of Theorem mptexg
StepHypRef Expression
1 funmpt 5629 . 2
2 eqid 2457 . . . 4
32dmmptss 5508 . . 3
4 ssexg 4598 . . 3
53, 4mpan 670 . 2
6 funex 6140 . 2
71, 5, 6sylancr 663 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  e.wcel 1818   cvv 3109  C_wss 3475  e.cmpt 4510  domcdm 5004  Funwfun 5587
This theorem is referenced by:  mptex  6143  ovmpt3rab1  6534  offval  6547  abrexexg  6775  xpexgALT  6793  offval3  6794  mptsuppdifd  6941  suppssov1  6951  suppssfv  6955  mpt2curryvald  7018  iunon  7028  onoviun  7033  mptelixpg  7526  fsuppmptif  7879  sniffsupp  7889  cantnfrescl  8116  cantnfp1lem1  8118  cantnflem1  8129  infxpenc2lem2  8418  infxpenc2lem2OLD  8422  coftr  8674  axcc3  8839  seqof2  12165  reps  12742  wrd2f1tovbij  12898  ramcl  14547  restval  14824  prdsplusgval  14870  prdsmulrval  14872  prdsvscaval  14876  resf1st  15263  resf2nd  15264  funcres  15265  galactghm  16428  symgfixfolem1  16463  pmtrval  16476  pmtrrn  16482  pmtrfrn  16483  sylow1lem4  16621  sylow3lem2  16648  sylow3lem3  16649  gsummptfsaddOLD  16941  gsum2dlem2  16998  gsum2d  16999  dprdfinv  17059  dprdfadd  17060  dmdprdsplitlem  17084  dpjfval  17104  dpjidcl  17107  mptscmfsupp0  17576  psrass1lem  18029  psrridm  18058  psrcom  18064  mvrfval  18076  mplcoe5  18131  mplbas2  18134  opsrval  18139  evlslem6  18181  psropprmul  18279  evls1sca  18360  frlmgsumOLD  18801  frlmgsum  18802  frlmphllem  18811  uvcfval  18815  uvcval  18816  uvcff  18822  uvcresum  18824  matgsum  18939  mvmulval  19045  mavmuldm  19052  mavmul0g  19055  marepvval0  19068  mat2pmatfval  19224  cpm2mfval  19250  chpmatfval  19331  ntrfval  19525  clsfval  19526  neifval  19600  lpfval  19639  ptcnplem  20122  upxp  20124  xkocnv  20315  fmfnfmlem3  20457  fmfnfmlem4  20458  ptcmplem3  20554  ustuqtoplem  20742  ustuqtop0  20743  utopsnneiplem  20750  prdsdsf  20870  ressprdsds  20874  prdsxmslem2  21032  rrxmval  21832  tdeglem4  22458  tayl0  22757  itgulm2  22804  pserulm  22817  efabl  22937  efsubm  22938  lmif  24151  islmib  24153  nbgraf1o0  24446  cusgrafilem3  24481  wlkiswwlk2  24697  wwlkextbij  24733  clwlkisclwwlklem2  24786  clwlksizeeq  24852  vdgrfval  24895  frgrancvvdeqlem9  25041  numclwwlk2lem3  25106  grpoinvfval  25226  indv  28026  indval  28027  ofcfval  28097  ofcfval3  28101  omsval  28264  sitgclg  28284  ptpcon  28678  tailfval  30190  upixp  30220  pw2f1ocnv  30979  kelac1  31009  fmulcl  31575  fmuldfeqlem1  31576  dvnmul  31740  dvnprodlem2  31744  stoweidlem31  31813  stoweidlem42  31824  stoweidlem48  31830  etransclem1  32018  etransclem4  32021  etransclem13  32030  etransclem17  32034  funcrngcsetc  32806  funcringcsetc  32843  scmsuppss  32965  rmfsupp  32967  scmfsupp  32971  mptcfsupp  32973  lincresunit2  33079  bnj1366  33888
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