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

Theorem fconstmpt 4732
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 3655 . . . 4  |-  ( y  e.  { B }  <->  y  =  B )
21anbi2i 675 . . 3  |-  ( ( x  e.  A  /\  y  e.  { B } )  <->  ( x  e.  A  /\  y  =  B ) )
32opabbii 4083 . 2  |-  { <. x ,  y >.  |  ( x  e.  A  /\  y  e.  { B } ) }  =  { <. x ,  y
>.  |  ( x  e.  A  /\  y  =  B ) }
4 df-xp 4695 . 2  |-  ( A  X.  { B }
)  =  { <. x ,  y >.  |  ( x  e.  A  /\  y  e.  { B } ) }
5 df-mpt 4079 . 2  |-  ( x  e.  A  |->  B )  =  { <. x ,  y >.  |  ( x  e.  A  /\  y  =  B ) }
63, 4, 53eqtr4i 2313 1  |-  ( A  X.  { B }
)  =  ( x  e.  A  |->  B )
Colors of variables: wff set class
Syntax hints:    /\ wa 358    = wceq 1623    e. wcel 1684   {csn 3640   {copab 4076    e. cmpt 4077    X. cxp 4687
This theorem is referenced by:  fconst  5427  fcoconst  5695  fmptsn  5709  xpexgALT  6070  ofc12  6102  caofinvl  6104  cantnf  7395  cnfcom2lem  7404  harmonic  12317  geomulcvg  12332  vdwlem8  13035  ramcl  13076  pwsvscafval  13393  setcepi  13920  diag2  14019  pws0g  14408  0frgp  15088  pwsgsum  15230  lmhmvsca  15802  rrgsupp  16032  psrlinv  16142  psrass23  16154  mplcoe1  16209  mplcoe3  16210  mplcoe2  16211  mplmon2  16234  evlslem2  16249  coe1z  16340  coe1mul2lem1  16344  coe1tm  16349  coe1sclmul  16358  coe1sclmul2  16360  pttoponconst  17292  cnmptc  17356  cnmptkc  17373  pt1hmeo  17497  tmdgsum2  17779  resspwsds  17936  imasdsf1olem  17937  nmoeq0  18245  idnghm  18252  ovolctb  18849  ovoliunnul  18866  vitalilem4  18966  vitalilem5  18967  ismbf  18985  mbfconst  18990  mbfss  19001  mbfmulc2re  19003  mbfneg  19005  mbfmulc2  19018  itg11  19046  itg2const  19095  itg2mulclem  19101  itg2mulc  19102  itg2monolem1  19105  itg0  19134  itgz  19135  itgvallem3  19140  iblposlem  19146  i1fibl  19162  itgitg1  19163  itgge0  19165  iblconst  19172  itgconst  19173  itgfsum  19181  iblmulc2  19185  itgmulc2lem1  19186  bddmulibl  19193  dvcmulf  19294  dvexp  19302  dvexp2  19303  dvmptid  19306  dvmptc  19307  dvef  19327  rolle  19337  dv11cn  19348  ftc1lem4  19386  ftc2  19391  evlslem1  19399  evl1sca  19413  tdeglem4  19446  ply1nzb  19508  plyconst  19588  plyeq0lem  19592  plypf1  19594  coeeulem  19606  plyco  19623  0dgr  19627  0dgrb  19628  dgrcolem2  19655  dgrco  19656  plyremlem  19684  elqaalem3  19701  iaa  19705  taylply2  19747  itgulm  19784  amgmlem  20284  ftalem7  20316  basellem8  20325  dchrfi  20494  bra0  22530  xrge0mulc1cn  23323  esumnul  23427  esum0  23428  esumcvg  23454  ofcc  23467  mbfmcst  23564  0rrv  23654  txsconlem  23771  cvmliftphtlem  23848  repwsmet  26558  rrnequiv  26559  mzpconstmpt  26818  mzpcompact2lem  26829  uvcresum  27242  grpvrinv  27451  mendlmod  27501  mendassa  27502  expgrowthi  27550  expgrowth  27552  stoweidlem21  27770
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-sn 3646  df-opab 4078  df-mpt 4079  df-xp 4695
  Copyright terms: Public domain W3C validator