Theorem fconstmpt 4894

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.

Step	Hyp	Ref	Expression
1		elsn 3903	. . . 4 |- ( y e. { B } <-> y = B )
2	1	anbi2i 694	. . 3 |- ( ( x e. A /\ y e. { B } ) <-> ( x e. A /\ y = B ) )
3	2	opabbii 4368	. 2 |- { <. x , y >. | ( x e. A /\ y e. { B } ) } = { <. x , y >. | ( x e. A /\ y = B ) }
4		df-xp 4858	. 2 |- ( A X. { B } ) = { <. x , y >. | ( x e. A /\ y e. { B } ) }
5		df-mpt 4364	. 2 |- ( x e. A |-> B ) = { <. x , y >. | ( x e. A /\ y = B ) }
6	3, 4, 5	3eqtr4i 2473	1 |- ( A X. { B } ) = ( x e. A |-> B )

Syntax hints:   /\ wa 369   = wceq 1369   e. wcel 1756   {csn 3889   {copab 4361   e. cmpt 4362   X. cxp 4850

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-sn 3890  df-opab 4363  df-mpt 4364  df-xp 4858

This theorem is referenced by:  fconst  5608  fcoconst  5892  fmptsn  5911  fconstmpt2  6197  ofc12  6357  caofinvl  6359  xpexgALT  6582  cantnf  7913  cantnfOLD  7935  cnfcom2lem  7946  cnfcom2lemOLD  7954  repsconst  12422  harmonic  13333  geomulcvg  13348  vdwlem8  14061  ramcl  14102  pwsvscafval  14444  setcepi  14968  diag2  15067  pws0g  15469  0frgp  16288  pwsgsum  16485  pwsgsumOLD  16486  lmhmvsca  17138  rrgsupp  17374  rrgsuppOLD  17375  psrlinv  17480  psrlidm  17486  psrridm  17488  psrass23  17494  mplcoe1  17556  mplcoe3  17557  mplcoe3OLD  17558  mplcoe5  17560  mplcoe2OLD  17562  mplmon2  17587  evlslem2  17609  evlslem1  17613  coe1z  17729  coe1mul2lem1  17733  coe1tm  17738  coe1sclmul  17747  coe1sclmul2  17749  evls1sca  17770  evl1sca  17780  uvcresum  18230  grpvrinv  18308  mdetunilem9  18438  pttoponconst  19182  cnmptc  19247  cnmptkc  19264  pt1hmeo  19391  tmdgsum2  19679  tsms0  19727  tgptsmscls  19736  resspwsds  19959  imasdsf1olem  19960  nmoeq0  20327  idnghm  20334  rrxcph  20908  ovolctb  20985  ovoliunnul  21002  vitalilem4  21103  vitalilem5  21104  ismbf  21120  mbfconst  21125  mbfss  21136  mbfmulc2re  21138  mbfneg  21140  mbfmulc2  21153  itg11  21181  itg2const  21230  itg2mulclem  21236  itg2mulc  21237  itg2monolem1  21240  itg0  21269  itgz  21270  itgvallem3  21275  iblposlem  21281  i1fibl  21297  itgitg1  21298  itgge0  21300  iblconst  21307  itgconst  21308  itgfsum  21316  iblmulc2  21320  itgmulc2lem1  21321  bddmulibl  21328  dvcmulf  21431  dvexp  21439  dvexp2  21440  dvmptid  21443  dvmptc  21444  dvef  21464  rolle  21474  dv11cn  21485  ftc1lem4  21523  ftc2  21528  tdeglem4  21541  ply1nzb  21606  plyconst  21686  plyeq0lem  21690  plypf1  21692  coeeulem  21704  plyco  21721  0dgr  21725  0dgrb  21726  dgrcolem2  21753  dgrco  21754  plyremlem  21782  elqaalem3  21799  iaa  21803  taylply2  21845  itgulm  21885  amgmlem  22395  ftalem7  22428  basellem8  22437  dchrfi  22606  dchrptlem3  22617  bra0  25366  xrge0mulc1cn  26383  esumnul  26514  esum0  26515  esumcvg  26547  ofcc  26560  mbfmcst  26686  sibf0  26732  0rrv  26846  ccatmulgnn0dir  26952  plymul02  26959  plymulx  26961  lgam1  27062  txsconlem  27141  cvmliftphtlem  27218  faclim  27564  ovoliunnfl  28445  voliunnfl  28447  volsupnfl  28448  itg2addnclem  28455  iblmulc2nc  28469  itgmulc2nclem1  28470  itgmulc2nclem2  28471  itgmulc2nc  28472  itgabsnc  28473  bddiblnc  28474  ftc1cnnclem  28477  ftc1anclem3  28481  ftc1anclem5  28483  ftc1anclem7  28485  ftc1anclem8  28486  ftc2nc  28488  repwsmet  28745  rrnequiv  28746  mzpconstmpt  29088  mzpcompact2lem  29100  mendlmod  29562  mendassa  29563  expgrowthi  29619  expgrowth  29621  stoweidlem21  29828  psrass23l  30836  lindsrng01  31014