Theorem fconstmpt 4881

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 3984	. . . 4 |- ( y e. { B } <-> y = B )
2	1	anbi2i 701	. . 3 |- ( ( x e. A /\ y e. { B } ) <-> ( x e. A /\ y = B ) )
3	2	opabbii 4470	. 2 |- { <. x , y >. | ( x e. A /\ y e. { B } ) } = { <. x , y >. | ( x e. A /\ y = B ) }
4		df-xp 4843	. 2 |- ( A X. { B } ) = { <. x , y >. | ( x e. A /\ y e. { B } ) }
5		df-mpt 4466	. 2 |- ( x e. A |-> B ) = { <. x , y >. | ( x e. A /\ y = B ) }
6	3, 4, 5	3eqtr4i 2485	1 |- ( A X. { B } ) = ( x e. A |-> B )

Syntax hints:   /\ wa 371   = wceq 1446   e. wcel 1889   {csn 3970   {copab 4463   |-> cmpt 4464   X. cxp 4835

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1671  ax-4 1684  ax-5 1760  ax-6 1807  ax-7 1853  ax-10 1917  ax-11 1922  ax-12 1935  ax-13 2093  ax-ext 2433

This theorem depends on definitions:  df-bi 189  df-an 373  df-tru 1449  df-ex 1666  df-nf 1670  df-sb 1800  df-clab 2440  df-cleq 2446  df-clel 2449  df-sn 3971  df-opab 4465  df-mpt 4466  df-xp 4843

This theorem is referenced by:  fconst  5774  fcoconst  6065  fmptsn  6089  fconstmpt2  6396  ofc12  6561  caofinvl  6563  xpexgALT  6791  cantnf  8203  cnfcom2lem  8211  repsconst  12882  harmonic  13929  geomulcvg  13944  vdwlem8  14950  ramcl  14999  pwsvscafval  15404  setcepi  15995  diag2  16142  pws0g  16584  0frgp  17441  pwsgsum  17623  lmhmvsca  18280  rrgsupp  18527  psrlinv  18633  psrlidm  18639  psrridm  18640  psrass23l  18644  psrass23  18646  mplcoe1  18701  mplcoe3  18702  mplcoe5  18704  mplmon2  18728  evlslem2  18747  evlslem1  18750  coe1z  18868  coe1mul2lem1  18872  coe1tm  18878  coe1sclmul  18887  coe1sclmul2  18889  evls1sca  18924  evl1sca  18934  uvcresum  19363  grpvrinv  19433  mdetunilem9  19657  pttoponconst  20624  cnmptc  20689  cnmptkc  20706  pt1hmeo  20833  tmdgsum2  21123  tsms0  21168  tgptsmscls  21176  resspwsds  21399  imasdsf1olem  21400  nmoeq0  21769  idnghm  21776  rrxcph  22363  ovolctb  22455  ovoliunnul  22472  vitalilem4  22581  vitalilem5  22582  ismbf  22598  mbfconst  22603  mbfss  22614  mbfmulc2re  22616  mbfneg  22618  mbfmulc2  22631  itg11  22661  itg2const  22710  itg2mulclem  22716  itg2mulc  22717  itg2monolem1  22720  itg0  22749  itgz  22750  itgvallem3  22755  iblposlem  22761  i1fibl  22777  itgitg1  22778  itgge0  22780  iblconst  22787  itgconst  22788  itgfsum  22796  iblmulc2  22800  itgmulc2lem1  22801  bddmulibl  22808  dvcmulf  22911  dvexp  22919  dvexp2  22920  dvmptid  22923  dvmptc  22924  dvef  22944  rolle  22954  dv11cn  22965  ftc1lem4  23003  ftc2  23008  tdeglem4  23021  ply1nzb  23083  plyconst  23172  plyeq0lem  23176  plypf1  23178  coeeulem  23190  plyco  23207  0dgr  23211  0dgrb  23212  dgrcolem2  23240  dgrco  23241  plyremlem  23269  elqaalem3  23286  elqaalem3OLD  23289  iaa  23293  taylply2  23335  itgulm  23375  amgmlem  23927  lgam1  24001  ftalem7  24017  basellem8  24026  dchrfi  24195  dchrptlem3  24206  bra0  27615  padct  28319  xrge0mulc1cn  28759  esumnul  28881  esum0  28882  esumcvg  28919  ofcc  28939  mbfmcst  29093  sibf0  29179  0rrv  29296  ccatmulgnn0dir  29440  plymul02  29447  plymulx  29449  txsconlem  29975  cvmliftphtlem  30052  faclim  30394  poimirlem30  31982  ovoliunnfl  31994  voliunnfl  31996  volsupnfl  31997  itg2addnclem  32005  iblmulc2nc  32019  itgmulc2nclem1  32020  itgmulc2nclem2  32021  itgmulc2nc  32022  itgabsnc  32023  bddiblnc  32024  ftc1cnnclem  32027  ftc1anclem3  32031  ftc1anclem5  32033  ftc1anclem7  32035  ftc1anclem8  32036  ftc2nc  32038  repwsmet  32178  rrnequiv  32179  mzpconstmpt  35594  mzpcompact2lem  35605  mendlmod  36071  mendassa  36072  expgrowthi  36693  expgrowth  36695  binomcxplemrat  36710  binomcxplemnotnn0  36716  rnmptc  37447  iblconstmpt  37842  iblempty  37852  itgiccshift  37867  itgperiod  37868  itgsbtaddcnst  37869  stoweidlem21  37891  lindsrng01  40365  aacllem  40644