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

Theorem fconstmpt 4924
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 3831 . . . 4  |-  ( y  e.  { B }  <->  y  =  B )
21anbi2i 677 . . 3  |-  ( ( x  e.  A  /\  y  e.  { B } )  <->  ( x  e.  A  /\  y  =  B ) )
32opabbii 4275 . 2  |-  { <. x ,  y >.  |  ( x  e.  A  /\  y  e.  { B } ) }  =  { <. x ,  y
>.  |  ( x  e.  A  /\  y  =  B ) }
4 df-xp 4887 . 2  |-  ( A  X.  { B }
)  =  { <. x ,  y >.  |  ( x  e.  A  /\  y  e.  { B } ) }
5 df-mpt 4271 . 2  |-  ( x  e.  A  |->  B )  =  { <. x ,  y >.  |  ( x  e.  A  /\  y  =  B ) }
63, 4, 53eqtr4i 2468 1  |-  ( A  X.  { B }
)  =  ( x  e.  A  |->  B )
Colors of variables: wff set class
Syntax hints:    /\ wa 360    = wceq 1653    e. wcel 1726   {csn 3816   {copab 4268    e. cmpt 4269    X. cxp 4879
This theorem is referenced by:  fconst  5632  fcoconst  5908  fmptsn  5925  xpexgALT  6300  ofc12  6332  caofinvl  6334  cantnf  7652  cnfcom2lem  7661  harmonic  12643  geomulcvg  12658  vdwlem8  13361  ramcl  13402  pwsvscafval  13721  setcepi  14248  diag2  14347  pws0g  14736  0frgp  15416  pwsgsum  15558  lmhmvsca  16126  rrgsupp  16356  psrlinv  16466  psrass23  16478  mplcoe1  16533  mplcoe3  16534  mplcoe2  16535  mplmon2  16558  evlslem2  16573  coe1z  16661  coe1mul2lem1  16665  coe1tm  16670  coe1sclmul  16679  coe1sclmul2  16681  pttoponconst  17634  cnmptc  17699  cnmptkc  17716  pt1hmeo  17843  tmdgsum2  18131  resspwsds  18407  imasdsf1olem  18408  nmoeq0  18775  idnghm  18782  ovolctb  19391  ovoliunnul  19408  vitalilem4  19508  vitalilem5  19509  ismbf  19525  mbfconst  19530  mbfss  19541  mbfmulc2re  19543  mbfneg  19545  mbfmulc2  19558  itg11  19586  itg2const  19635  itg2mulclem  19641  itg2mulc  19642  itg2monolem1  19645  itg0  19674  itgz  19675  itgvallem3  19680  iblposlem  19686  i1fibl  19702  itgitg1  19703  itgge0  19705  iblconst  19712  itgconst  19713  itgfsum  19721  iblmulc2  19725  itgmulc2lem1  19726  bddmulibl  19733  dvcmulf  19836  dvexp  19844  dvexp2  19845  dvmptid  19848  dvmptc  19849  dvef  19869  rolle  19879  dv11cn  19890  ftc1lem4  19928  ftc2  19933  evlslem1  19941  evl1sca  19955  tdeglem4  19988  ply1nzb  20050  plyconst  20130  plyeq0lem  20134  plypf1  20136  coeeulem  20148  plyco  20165  0dgr  20169  0dgrb  20170  dgrcolem2  20197  dgrco  20198  plyremlem  20226  elqaalem3  20243  iaa  20247  taylply2  20289  itgulm  20329  amgmlem  20833  ftalem7  20866  basellem8  20875  dchrfi  21044  bra0  23458  xrge0mulc1cn  24332  esumnul  24448  esum0  24449  esumcvg  24481  ofcc  24494  mbfmcst  24614  sibf0  24654  0rrv  24714  lgam1  24853  txsconlem  24932  cvmliftphtlem  25009  faclim  25370  ovoliunnfl  26260  voliunnfl  26262  volsupnfl  26263  itg2addnclem  26270  iblmulc2nc  26284  itgmulc2nclem1  26285  itgmulc2nclem2  26286  itgmulc2nc  26287  itgabsnc  26288  bddiblnc  26289  ftc1cnnclem  26292  ftc1anclem3  26296  ftc1anclem5  26298  ftc1anclem7  26300  ftc1anclem8  26301  ftc2nc  26303  repwsmet  26557  rrnequiv  26558  mzpconstmpt  26811  mzpcompact2lem  26822  uvcresum  27233  grpvrinv  27442  mendlmod  27492  mendassa  27493  expgrowthi  27541  expgrowth  27543  stoweidlem21  27760
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-sn 3822  df-opab 4270  df-mpt 4271  df-xp 4887
  Copyright terms: Public domain W3C validator