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

Theorem fconstmpt 4863
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 3774 . . . 4  |-  ( y  e.  { B }  <->  y  =  B )
21anbi2i 676 . . 3  |-  ( ( x  e.  A  /\  y  e.  { B } )  <->  ( x  e.  A  /\  y  =  B ) )
32opabbii 4215 . 2  |-  { <. x ,  y >.  |  ( x  e.  A  /\  y  e.  { B } ) }  =  { <. x ,  y
>.  |  ( x  e.  A  /\  y  =  B ) }
4 df-xp 4826 . 2  |-  ( A  X.  { B }
)  =  { <. x ,  y >.  |  ( x  e.  A  /\  y  e.  { B } ) }
5 df-mpt 4211 . 2  |-  ( x  e.  A  |->  B )  =  { <. x ,  y >.  |  ( x  e.  A  /\  y  =  B ) }
63, 4, 53eqtr4i 2419 1  |-  ( A  X.  { B }
)  =  ( x  e.  A  |->  B )
Colors of variables: wff set class
Syntax hints:    /\ wa 359    = wceq 1649    e. wcel 1717   {csn 3759   {copab 4208    e. cmpt 4209    X. cxp 4818
This theorem is referenced by:  fconst  5571  fcoconst  5846  fmptsn  5863  xpexgALT  6238  ofc12  6270  caofinvl  6272  cantnf  7584  cnfcom2lem  7593  harmonic  12567  geomulcvg  12582  vdwlem8  13285  ramcl  13326  pwsvscafval  13645  setcepi  14172  diag2  14271  pws0g  14660  0frgp  15340  pwsgsum  15482  lmhmvsca  16050  rrgsupp  16280  psrlinv  16390  psrass23  16402  mplcoe1  16457  mplcoe3  16458  mplcoe2  16459  mplmon2  16482  evlslem2  16497  coe1z  16585  coe1mul2lem1  16589  coe1tm  16594  coe1sclmul  16603  coe1sclmul2  16605  pttoponconst  17552  cnmptc  17617  cnmptkc  17634  pt1hmeo  17761  tmdgsum2  18049  resspwsds  18312  imasdsf1olem  18313  nmoeq0  18643  idnghm  18650  ovolctb  19255  ovoliunnul  19272  vitalilem4  19372  vitalilem5  19373  ismbf  19391  mbfconst  19396  mbfss  19407  mbfmulc2re  19409  mbfneg  19411  mbfmulc2  19424  itg11  19452  itg2const  19501  itg2mulclem  19507  itg2mulc  19508  itg2monolem1  19511  itg0  19540  itgz  19541  itgvallem3  19546  iblposlem  19552  i1fibl  19568  itgitg1  19569  itgge0  19571  iblconst  19578  itgconst  19579  itgfsum  19587  iblmulc2  19591  itgmulc2lem1  19592  bddmulibl  19599  dvcmulf  19700  dvexp  19708  dvexp2  19709  dvmptid  19712  dvmptc  19713  dvef  19733  rolle  19743  dv11cn  19754  ftc1lem4  19792  ftc2  19797  evlslem1  19805  evl1sca  19819  tdeglem4  19852  ply1nzb  19914  plyconst  19994  plyeq0lem  19998  plypf1  20000  coeeulem  20012  plyco  20029  0dgr  20033  0dgrb  20034  dgrcolem2  20061  dgrco  20062  plyremlem  20090  elqaalem3  20107  iaa  20111  taylply2  20153  itgulm  20193  amgmlem  20697  ftalem7  20730  basellem8  20739  dchrfi  20908  bra0  23303  xrge0mulc1cn  24133  esumnul  24241  esum0  24242  esumcvg  24274  ofcc  24287  mbfmcst  24405  0rrv  24490  lgam1  24629  txsconlem  24708  cvmliftphtlem  24785  faclim  25125  ovoliunnfl  25955  voliunnfl  25957  volsupnfl  25958  itg2addnclem  25959  itg2addnc  25961  itgaddnclem2  25966  iblmulc2nc  25972  itgmulc2nclem1  25973  itgmulc2nclem2  25974  itgmulc2nc  25975  itgabsnc  25976  bddiblnc  25977  ftc1cnnclem  25980  repwsmet  26236  rrnequiv  26237  mzpconstmpt  26490  mzpcompact2lem  26501  uvcresum  26913  grpvrinv  27122  mendlmod  27172  mendassa  27173  expgrowthi  27221  expgrowth  27223  stoweidlem21  27440
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2370
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2376  df-cleq 2382  df-clel 2385  df-sn 3765  df-opab 4210  df-mpt 4211  df-xp 4826
  Copyright terms: Public domain W3C validator