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

Theorem mptexg 6125
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 5607 . 2  |-  Fun  (
x  e.  A  |->  B )
2 eqid 2404 . . . 4  |-  ( x  e.  A  |->  B )  =  ( x  e.  A  |->  B )
32dmmptss 5321 . . 3  |-  dom  (
x  e.  A  |->  B )  C_  A
4 ssexg 4542 . . 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 6123 . 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 1844   _Vcvv 3061    C_ wss 3416    |-> cmpt 4455   dom cdm 4825   Fun wfun 5565
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1641  ax-4 1654  ax-5 1727  ax-6 1773  ax-7 1816  ax-9 1848  ax-10 1863  ax-11 1868  ax-12 1880  ax-13 2028  ax-ext 2382  ax-rep 4509  ax-sep 4519  ax-nul 4527  ax-pr 4632
This theorem depends on definitions:  df-bi 187  df-or 370  df-an 371  df-3an 978  df-tru 1410  df-ex 1636  df-nf 1640  df-sb 1766  df-eu 2244  df-mo 2245  df-clab 2390  df-cleq 2396  df-clel 2399  df-nfc 2554  df-ne 2602  df-ral 2761  df-rex 2762  df-reu 2763  df-rab 2765  df-v 3063  df-sbc 3280  df-csb 3376  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-nul 3741  df-if 3888  df-sn 3975  df-pr 3977  df-op 3981  df-uni 4194  df-iun 4275  df-br 4398  df-opab 4456  df-mpt 4457  df-id 4740  df-xp 4831  df-rel 4832  df-cnv 4833  df-co 4834  df-dm 4835  df-rn 4836  df-res 4837  df-ima 4838  df-iota 5535  df-fun 5573  df-fn 5574  df-f 5575  df-f1 5576  df-fo 5577  df-f1o 5578  df-fv 5579
This theorem is referenced by:  mptex  6126  ovmpt3rab1  6517  offval  6530  abrexexg  6761  xpexgALT  6779  offval3  6780  mptsuppdifd  6927  suppssov1  6937  suppssfv  6941  mpt2curryvald  7004  iunon  7044  onoviun  7049  mptelixpg  7546  fsuppmptif  7895  sniffsupp  7905  cantnfrescl  8129  cantnfp1lem1  8131  cantnflem1  8142  infxpenc2lem2  8431  infxpenc2lem2OLD  8435  coftr  8687  axcc3  8852  seqof2  12211  reps  12800  wrd2f1tovbij  12956  ramcl  14758  restval  15043  prdsplusgval  15089  prdsmulrval  15091  prdsvscaval  15095  resf1st  15509  resf2nd  15510  funcres  15511  galactghm  16754  symgfixfolem1  16789  pmtrval  16802  pmtrrn  16808  pmtrfrn  16809  sylow1lem4  16947  sylow3lem2  16974  sylow3lem3  16975  gsummptfsaddOLD  17267  gsum2dlem2  17321  gsum2d  17322  dprdfinv  17381  dprdfadd  17382  dmdprdsplitlem  17406  dpjfval  17426  dpjidcl  17429  mptscmfsupp0  17898  psrass1lem  18351  psrridm  18380  psrcom  18386  mvrfval  18398  mplcoe5  18453  mplbas2  18456  opsrval  18461  evlslem6  18503  psropprmul  18601  evls1sca  18682  frlmgsumOLD  19099  frlmgsum  19100  frlmphllem  19109  uvcfval  19113  uvcval  19114  uvcff  19120  uvcresum  19122  matgsum  19233  mvmulval  19339  mavmuldm  19346  mavmul0g  19349  marepvval0  19362  mat2pmatfval  19518  cpm2mfval  19544  chpmatfval  19625  ntrfval  19819  clsfval  19820  neifval  19895  lpfval  19934  ptcnplem  20416  upxp  20418  xkocnv  20609  fmfnfmlem3  20751  fmfnfmlem4  20752  ptcmplem3  20848  ustuqtoplem  21036  ustuqtop0  21037  utopsnneiplem  21044  prdsdsf  21164  ressprdsds  21168  prdsxmslem2  21326  rrxmval  22126  tdeglem4  22752  tayl0  23051  itgulm2  23098  pserulm  23111  efabl  23231  efsubm  23232  lmif  24546  islmib  24548  nbgraf1o0  24875  cusgrafilem3  24910  wlkiswwlk2  25126  wwlkextbij  25162  clwlkisclwwlklem2  25215  clwlksizeeq  25281  vdgrfval  25324  frgrancvvdeqlem9  25470  numclwwlk2lem3  25535  grpoinvfval  25653  acunirnmpt  27956  acunirnmpt2  27957  acunirnmpt2f  27958  aciunf1lem  27959  indv  28473  indval  28474  ofcfval  28558  ofcfval3  28562  omsval  28754  carsgclctunlem2  28780  pmeasadd  28786  sitgclg  28803  bnj1366  29228  ptpcon  29543  fwddifval  30513  tailfval  30613  upixp  31515  pw2f1ocnv  35354  kelac1  35384  fmulcl  36956  fmuldfeqlem1  36957  dvnmul  37121  dvnprodlem2  37125  stoweidlem31  37194  stoweidlem42  37205  stoweidlem48  37211  etransclem1  37399  etransclem4  37402  etransclem13  37411  etransclem17  37415  funcrngcsetc  38330  funcringcsetc  38367  scmsuppss  38489  rmfsupp  38491  scmfsupp  38495  mptcfsupp  38497  lincresunit2  38603  offval0  38635
  Copyright terms: Public domain W3C validator