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

Theorem fconstmpt 4748
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 3668 . . . 4  |-  ( y  e.  { B }  <->  y  =  B )
21anbi2i 675 . . 3  |-  ( ( x  e.  A  /\  y  e.  { B } )  <->  ( x  e.  A  /\  y  =  B ) )
32opabbii 4099 . 2  |-  { <. x ,  y >.  |  ( x  e.  A  /\  y  e.  { B } ) }  =  { <. x ,  y
>.  |  ( x  e.  A  /\  y  =  B ) }
4 df-xp 4711 . 2  |-  ( A  X.  { B }
)  =  { <. x ,  y >.  |  ( x  e.  A  /\  y  e.  { B } ) }
5 df-mpt 4095 . 2  |-  ( x  e.  A  |->  B )  =  { <. x ,  y >.  |  ( x  e.  A  /\  y  =  B ) }
63, 4, 53eqtr4i 2326 1  |-  ( A  X.  { B }
)  =  ( x  e.  A  |->  B )
Colors of variables: wff set class
Syntax hints:    /\ wa 358    = wceq 1632    e. wcel 1696   {csn 3653   {copab 4092    e. cmpt 4093    X. cxp 4703
This theorem is referenced by:  fconst  5443  fcoconst  5711  fmptsn  5725  xpexgALT  6086  ofc12  6118  caofinvl  6120  cantnf  7411  cnfcom2lem  7420  harmonic  12333  geomulcvg  12348  vdwlem8  13051  ramcl  13092  pwsvscafval  13409  setcepi  13936  diag2  14035  pws0g  14424  0frgp  15104  pwsgsum  15246  lmhmvsca  15818  rrgsupp  16048  psrlinv  16158  psrass23  16170  mplcoe1  16225  mplcoe3  16226  mplcoe2  16227  mplmon2  16250  evlslem2  16265  coe1z  16356  coe1mul2lem1  16360  coe1tm  16365  coe1sclmul  16374  coe1sclmul2  16376  pttoponconst  17308  cnmptc  17372  cnmptkc  17389  pt1hmeo  17513  tmdgsum2  17795  resspwsds  17952  imasdsf1olem  17953  nmoeq0  18261  idnghm  18268  ovolctb  18865  ovoliunnul  18882  vitalilem4  18982  vitalilem5  18983  ismbf  19001  mbfconst  19006  mbfss  19017  mbfmulc2re  19019  mbfneg  19021  mbfmulc2  19034  itg11  19062  itg2const  19111  itg2mulclem  19117  itg2mulc  19118  itg2monolem1  19121  itg0  19150  itgz  19151  itgvallem3  19156  iblposlem  19162  i1fibl  19178  itgitg1  19179  itgge0  19181  iblconst  19188  itgconst  19189  itgfsum  19197  iblmulc2  19201  itgmulc2lem1  19202  bddmulibl  19209  dvcmulf  19310  dvexp  19318  dvexp2  19319  dvmptid  19322  dvmptc  19323  dvef  19343  rolle  19353  dv11cn  19364  ftc1lem4  19402  ftc2  19407  evlslem1  19415  evl1sca  19429  tdeglem4  19462  ply1nzb  19524  plyconst  19604  plyeq0lem  19608  plypf1  19610  coeeulem  19622  plyco  19639  0dgr  19643  0dgrb  19644  dgrcolem2  19671  dgrco  19672  plyremlem  19700  elqaalem3  19717  iaa  19721  taylply2  19763  itgulm  19800  amgmlem  20300  ftalem7  20332  basellem8  20341  dchrfi  20510  bra0  22546  xrge0mulc1cn  23338  esumnul  23442  esum0  23443  esumcvg  23469  ofcc  23482  mbfmcst  23579  0rrv  23669  txsconlem  23786  cvmliftphtlem  23863  ovoliunnfl  25001  itg2addnclem  25003  itg2addnc  25005  itgaddnclem2  25010  iblmulc2nc  25016  itgmulc2nclem1  25017  itgmulc2nclem2  25018  itgmulc2nc  25019  itgabsnc  25020  bddiblnc  25021  ftc1cnnclem  25024  repwsmet  26661  rrnequiv  26662  mzpconstmpt  26921  mzpcompact2lem  26932  uvcresum  27345  grpvrinv  27554  mendlmod  27604  mendassa  27605  expgrowthi  27653  expgrowth  27655  stoweidlem21  27873
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-sn 3659  df-opab 4094  df-mpt 4095  df-xp 4711
  Copyright terms: Public domain W3C validator