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

Theorem fconstmpt 4913
Description: Representation of a constant function using the mapping operation. (Note that  x cannot appear free in  B.) (Contributed by NM, 12-Oct-1999.) (Revised by Mario Carneiro, 16-Nov-2013.)
Assertion
Ref Expression
fconstmpt  |-  ( A  X.  { B }
)  =  ( x  e.  A  |->  B )
Distinct variable groups:    x, A    x, B

Proof of Theorem fconstmpt
Dummy variable  y is distinct from all other variables.
StepHypRef Expression
1 elsn 3821 . . . 4  |-  ( y  e.  { B }  <->  y  =  B )
21anbi2i 676 . . 3  |-  ( ( x  e.  A  /\  y  e.  { B } )  <->  ( x  e.  A  /\  y  =  B ) )
32opabbii 4264 . 2  |-  { <. x ,  y >.  |  ( x  e.  A  /\  y  e.  { B } ) }  =  { <. x ,  y
>.  |  ( x  e.  A  /\  y  =  B ) }
4 df-xp 4876 . 2  |-  ( A  X.  { B }
)  =  { <. x ,  y >.  |  ( x  e.  A  /\  y  e.  { B } ) }
5 df-mpt 4260 . 2  |-  ( x  e.  A  |->  B )  =  { <. x ,  y >.  |  ( x  e.  A  /\  y  =  B ) }
63, 4, 53eqtr4i 2465 1  |-  ( A  X.  { B }
)  =  ( x  e.  A  |->  B )
Colors of variables: wff set class
Syntax hints:    /\ wa 359    = wceq 1652    e. wcel 1725   {csn 3806   {copab 4257    e. cmpt 4258    X. cxp 4868
This theorem is referenced by:  fconst  5621  fcoconst  5897  fmptsn  5914  xpexgALT  6289  ofc12  6321  caofinvl  6323  cantnf  7641  cnfcom2lem  7650  harmonic  12630  geomulcvg  12645  vdwlem8  13348  ramcl  13389  pwsvscafval  13708  setcepi  14235  diag2  14334  pws0g  14723  0frgp  15403  pwsgsum  15545  lmhmvsca  16113  rrgsupp  16343  psrlinv  16453  psrass23  16465  mplcoe1  16520  mplcoe3  16521  mplcoe2  16522  mplmon2  16545  evlslem2  16560  coe1z  16648  coe1mul2lem1  16652  coe1tm  16657  coe1sclmul  16666  coe1sclmul2  16668  pttoponconst  17621  cnmptc  17686  cnmptkc  17703  pt1hmeo  17830  tmdgsum2  18118  resspwsds  18394  imasdsf1olem  18395  nmoeq0  18762  idnghm  18769  ovolctb  19378  ovoliunnul  19395  vitalilem4  19495  vitalilem5  19496  ismbf  19514  mbfconst  19519  mbfss  19530  mbfmulc2re  19532  mbfneg  19534  mbfmulc2  19547  itg11  19575  itg2const  19624  itg2mulclem  19630  itg2mulc  19631  itg2monolem1  19634  itg0  19663  itgz  19664  itgvallem3  19669  iblposlem  19675  i1fibl  19691  itgitg1  19692  itgge0  19694  iblconst  19701  itgconst  19702  itgfsum  19710  iblmulc2  19714  itgmulc2lem1  19715  bddmulibl  19722  dvcmulf  19823  dvexp  19831  dvexp2  19832  dvmptid  19835  dvmptc  19836  dvef  19856  rolle  19866  dv11cn  19877  ftc1lem4  19915  ftc2  19920  evlslem1  19928  evl1sca  19942  tdeglem4  19975  ply1nzb  20037  plyconst  20117  plyeq0lem  20121  plypf1  20123  coeeulem  20135  plyco  20152  0dgr  20156  0dgrb  20157  dgrcolem2  20184  dgrco  20185  plyremlem  20213  elqaalem3  20230  iaa  20234  taylply2  20276  itgulm  20316  amgmlem  20820  ftalem7  20853  basellem8  20862  dchrfi  21031  bra0  23445  xrge0mulc1cn  24319  esumnul  24435  esum0  24436  esumcvg  24468  ofcc  24481  mbfmcst  24601  sibf0  24641  0rrv  24701  lgam1  24840  txsconlem  24919  cvmliftphtlem  24996  faclim  25357  ovoliunnfl  26238  voliunnfl  26240  volsupnfl  26241  itg2addnclem  26246  iblmulc2nc  26260  itgmulc2nclem1  26261  itgmulc2nclem2  26262  itgmulc2nc  26263  itgabsnc  26264  bddiblnc  26265  ftc1cnnclem  26268  ftc1anclem3  26272  ftc1anclem5  26274  ftc1anclem7  26276  ftc1anclem8  26277  ftc2nc  26279  repwsmet  26534  rrnequiv  26535  mzpconstmpt  26788  mzpcompact2lem  26799  uvcresum  27210  grpvrinv  27419  mendlmod  27469  mendassa  27470  expgrowthi  27518  expgrowth  27520  stoweidlem21  27737
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-sn 3812  df-opab 4259  df-mpt 4260  df-xp 4876
  Copyright terms: Public domain W3C validator