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

Theorem mptexg 6128
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  |-  ( A  e.  V  ->  (
x  e.  A  |->  B )  e.  _V )
Distinct variable group:    x, A
Allowed substitution hints:    B( x)    V( x)

Proof of Theorem mptexg
StepHypRef Expression
1 funmpt 5622 . 2  |-  Fun  (
x  e.  A  |->  B )
2 eqid 2467 . . . 4  |-  ( x  e.  A  |->  B )  =  ( x  e.  A  |->  B )
32dmmptss 5501 . . 3  |-  dom  (
x  e.  A  |->  B )  C_  A
4 ssexg 4593 . . 3  |-  ( ( dom  ( x  e.  A  |->  B )  C_  A  /\  A  e.  V
)  ->  dom  ( x  e.  A  |->  B )  e.  _V )
53, 4mpan 670 . 2  |-  ( A  e.  V  ->  dom  ( x  e.  A  |->  B )  e.  _V )
6 funex 6126 . 2  |-  ( ( Fun  ( x  e.  A  |->  B )  /\  dom  ( x  e.  A  |->  B )  e.  _V )  ->  ( x  e.  A  |->  B )  e. 
_V )
71, 5, 6sylancr 663 1  |-  ( A  e.  V  ->  (
x  e.  A  |->  B )  e.  _V )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1767   _Vcvv 3113    C_ wss 3476    |-> cmpt 4505   dom cdm 4999   Fun wfun 5580
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-rep 4558  ax-sep 4568  ax-nul 4576  ax-pr 4686
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-ral 2819  df-rex 2820  df-reu 2821  df-rab 2823  df-v 3115  df-sbc 3332  df-csb 3436  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-nul 3786  df-if 3940  df-sn 4028  df-pr 4030  df-op 4034  df-uni 4246  df-iun 4327  df-br 4448  df-opab 4506  df-mpt 4507  df-id 4795  df-xp 5005  df-rel 5006  df-cnv 5007  df-co 5008  df-dm 5009  df-rn 5010  df-res 5011  df-ima 5012  df-iota 5549  df-fun 5588  df-fn 5589  df-f 5590  df-f1 5591  df-fo 5592  df-f1o 5593  df-fv 5594
This theorem is referenced by:  mptex  6129  ovmpt3rab1  6516  offval  6529  abrexexg  6756  xpexgALT  6774  offval3  6775  mptsuppdifd  6919  suppssov1  6929  suppssfv  6933  mpt2curryvald  6996  iunon  7006  onoviun  7011  mptelixpg  7503  fsuppmptif  7855  sniffsupp  7865  cantnfrescl  8091  cantnfp1lem1  8093  cantnflem1d  8103  cantnflem1  8104  infxpenc2lem2  8393  infxpenc2lem2OLD  8397  coftr  8649  axcc3  8814  seqof2  12128  reps  12699  wrd2f1tovbij  12855  ramcl  14399  restval  14675  prdsplusgval  14721  prdsmulrval  14723  prdsvscaval  14727  resf1st  15114  resf2nd  15115  funcres  15116  galactghm  16220  symgfixfolem1  16256  pmtrval  16269  pmtrrn  16275  pmtrfrn  16276  sylow1lem4  16414  sylow3lem2  16441  sylow3lem3  16442  gsummptfsaddOLD  16729  gsum2dlem2  16786  gsum2d  16787  dprdfinv  16846  dprdfadd  16847  dmdprdsplitlem  16871  dpjfval  16891  dpjidcl  16894  mptscmfsupp0  17356  psrass1lem  17797  psrridm  17826  psrdi  17829  psrdir  17830  psrcom  17832  mvrfval  17844  mplcoe5  17899  mplbas2  17902  opsrval  17907  evlslem6  17949  psropprmul  18047  evls1fval  18124  evls1sca  18128  frlmgsumOLD  18565  frlmgsum  18566  frlmphllem  18575  uvcfval  18579  uvcval  18580  uvcff  18586  uvcresum  18588  matgsum  18703  mvmulval  18809  mavmuldm  18816  mavmul0g  18819  marepvval0  18832  mat2pmatfval  18988  cpm2mfval  19014  chpmatfval  19095  ntrfval  19288  clsfval  19289  neifval  19363  lpfval  19402  ptcnplem  19854  upxp  19856  xkocnv  20047  fmfnfmlem3  20189  fmfnfmlem4  20190  ptcmplem3  20286  ustuqtoplem  20474  ustuqtop0  20475  utopsnneiplem  20482  prdsdsf  20602  ressprdsds  20606  prdsxmslem2  20764  rrxmval  21564  tdeglem4  22190  tayl0  22488  itgulm2  22535  pserulm  22548  lmif  23825  islmib  23827  nbgraf1o0  24119  cusgrafilem3  24154  wlkiswwlk2  24370  wwlkextbij  24406  clwlkisclwwlklem2  24459  clwlksizeeq  24525  vdgrfval  24568  frgrancvvdeqlem9  24715  numclwwlk2lem3  24780  grpoinvfval  24899  indv  27663  indval  27664  ofcfval  27734  ofcfval3  27738  omsval  27901  sitgclg  27921  ptpcon  28315  tailfval  29791  upixp  29821  pw2f1ocnv  30583  kelac1  30613  fmulcl  31131  fmuldfeqlem1  31132  dvcosax  31256  stoweidlem31  31331  stoweidlem42  31342  stoweidlem48  31348  scmsuppss  32038  rmfsupp  32040  scmfsupp  32044  mptcfsupp  32046  lincresunit2  32152  bnj1366  32967
  Copyright terms: Public domain W3C validator