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

Theorem mptexg 5944
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 5451 . 2  |-  Fun  (
x  e.  A  |->  B )
2 eqid 2441 . . . 4  |-  ( x  e.  A  |->  B )  =  ( x  e.  A  |->  B )
32dmmptss 5331 . . 3  |-  dom  (
x  e.  A  |->  B )  C_  A
4 ssexg 4435 . . 3  |-  ( ( dom  ( x  e.  A  |->  B )  C_  A  /\  A  e.  V
)  ->  dom  ( x  e.  A  |->  B )  e.  _V )
53, 4mpan 665 . 2  |-  ( A  e.  V  ->  dom  ( x  e.  A  |->  B )  e.  _V )
6 funex 5942 . 2  |-  ( ( Fun  ( x  e.  A  |->  B )  /\  dom  ( x  e.  A  |->  B )  e.  _V )  ->  ( x  e.  A  |->  B )  e. 
_V )
71, 5, 6sylancr 658 1  |-  ( A  e.  V  ->  (
x  e.  A  |->  B )  e.  _V )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1761   _Vcvv 2970    C_ wss 3325    e. cmpt 4347   dom cdm 4836   Fun wfun 5409
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-9 1765  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422  ax-rep 4400  ax-sep 4410  ax-nul 4418  ax-pr 4528
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 962  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1706  df-eu 2261  df-mo 2262  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-ne 2606  df-ral 2718  df-rex 2719  df-reu 2720  df-rab 2722  df-v 2972  df-sbc 3184  df-csb 3286  df-dif 3328  df-un 3330  df-in 3332  df-ss 3339  df-nul 3635  df-if 3789  df-sn 3875  df-pr 3877  df-op 3881  df-uni 4089  df-iun 4170  df-br 4290  df-opab 4348  df-mpt 4349  df-id 4632  df-xp 4842  df-rel 4843  df-cnv 4844  df-co 4845  df-dm 4846  df-rn 4847  df-res 4848  df-ima 4849  df-iota 5378  df-fun 5417  df-fn 5418  df-f 5419  df-f1 5420  df-fo 5421  df-f1o 5422  df-fv 5423
This theorem is referenced by:  mptex  5945  offval  6326  abrexexg  6551  xpexgALT  6569  offval3  6570  mptsuppdifd  6710  suppssov1  6720  suppssfv  6724  iunon  6795  onoviun  6800  mptelixpg  7296  fsuppmptif  7645  sniffsupp  7655  cantnfrescl  7880  cantnfp1lem1  7882  cantnflem1d  7892  cantnflem1  7893  infxpenc2lem2  8182  infxpenc2lem2OLD  8186  coftr  8438  axcc3  8603  seqof2  11860  reps  12404  ramcl  14086  restval  14361  prdsplusgval  14407  prdsmulrval  14409  prdsvscaval  14413  resf1st  14800  resf2nd  14801  funcres  14802  galactghm  15901  symgfixfolem1  15937  pmtrval  15950  pmtrrn  15956  pmtrfrn  15957  sylow1lem4  16093  sylow3lem2  16120  sylow3lem3  16121  gsummptfsaddOLD  16408  gsum2dlem2  16452  gsum2d  16453  dprdfinv  16499  dprdfadd  16500  dmdprdsplitlem  16524  dpjfval  16544  dpjidcl  16547  psrass1lem  17425  psrridm  17454  psrdi  17457  psrdir  17458  psrcom  17459  mvrfval  17471  mplcoe2  17525  mplbas2  17527  opsrval  17532  evlslem6  17574  psropprmul  17668  evls1fval  17727  evls1sca  17731  frlmgsumOLD  18154  frlmgsum  18155  frlmphllem  18164  uvcfval  18168  uvcval  18169  uvcff  18175  uvcresum  18177  mvmulval  18313  mavmuldm  18320  mavmul0g  18323  marepvval0  18336  ntrfval  18587  clsfval  18588  neifval  18662  lpfval  18701  ptcnplem  19153  upxp  19155  xkocnv  19346  fmfnfmlem3  19488  fmfnfmlem4  19489  ptcmplem3  19585  ustuqtoplem  19773  ustuqtop0  19774  utopsnneiplem  19781  prdsdsf  19901  ressprdsds  19905  prdsxmslem2  20063  rrxmval  20863  tdeglem4  21488  tayl0  21786  itgulm2  21833  pserulm  21846  nbgraf1o0  23290  cusgrafilem3  23324  vdgrfval  23500  grpoinvfval  23646  indv  26405  indval  26406  ofcfval  26476  ofcfval3  26480  ptpcon  27052  tailfval  28518  upixp  28548  pw2f1ocnv  29311  kelac1  29341  fmulcl  29687  fmuldfeqlem1  29688  stoweidlem31  29751  stoweidlem42  29762  stoweidlem48  29768  ovmpt3rab1  30086  wrd2f1tovbij  30180  wlkiswwlk2  30256  wwlkextbij  30290  clwlkisclwwlklem2  30373  clwlksizeeq  30450  frgrancvvdeqlem9  30559  numclwwlk2lem3  30624  scmsuppss  30702  rmfsupp  30704  scmfsupp  30708  mptcfsupp  30710  mptscmfsuppd  30711  lincresunit2  30853  bnj1366  31657
  Copyright terms: Public domain W3C validator