Theorem fconstmpt 4957

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 3958	. . . 4 |- ( y e. { B } <-> y = B )
2	1	anbi2i 692	. . 3 |- ( ( x e. A /\ y e. { B } ) <-> ( x e. A /\ y = B ) )
3	2	opabbii 4431	. 2 |- { <. x , y >. | ( x e. A /\ y e. { B } ) } = { <. x , y >. | ( x e. A /\ y = B ) }
4		df-xp 4919	. 2 |- ( A X. { B } ) = { <. x , y >. | ( x e. A /\ y e. { B } ) }
5		df-mpt 4427	. 2 |- ( x e. A |-> B ) = { <. x , y >. | ( x e. A /\ y = B ) }
6	3, 4, 5	3eqtr4i 2421	1 |- ( A X. { B } ) = ( x e. A |-> B )

Syntax hints:   /\ wa 367   = wceq 1399   e. wcel 1826   {csn 3944   {copab 4424   |-> cmpt 4425   X. cxp 4911

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360

This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1402  df-ex 1621  df-nf 1625  df-sb 1748  df-clab 2368  df-cleq 2374  df-clel 2377  df-sn 3945  df-opab 4426  df-mpt 4427  df-xp 4919

This theorem is referenced by:  fconst  5679  fcoconst  5970  fmptsn  5993  fconstmpt2  6296  ofc12  6464  caofinvl  6466  xpexgALT  6692  cantnf  8025  cantnfOLD  8047  cnfcom2lem  8058  cnfcom2lemOLD  8066  repsconst  12655  harmonic  13672  geomulcvg  13687  vdwlem8  14508  ramcl  14549  pwsvscafval  14901  setcepi  15484  diag2  15631  pws0g  16073  0frgp  16914  pwsgsum  17122  pwsgsumOLD  17123  lmhmvsca  17804  rrgsupp  18052  rrgsuppOLD  18053  psrlinv  18163  psrlidm  18169  psrridm  18171  psrass23l  18176  psrass23  18178  mplcoe1  18240  mplcoe3  18241  mplcoe3OLD  18242  mplcoe5  18244  mplcoe2OLD  18246  mplmon2  18271  evlslem2  18293  evlslem1  18297  coe1z  18417  coe1mul2lem1  18421  coe1tm  18427  coe1sclmul  18436  coe1sclmul2  18438  evls1sca  18473  evl1sca  18483  uvcresum  18913  grpvrinv  18983  mdetunilem9  19207  pttoponconst  20183  cnmptc  20248  cnmptkc  20265  pt1hmeo  20392  tmdgsum2  20680  tsms0  20728  tgptsmscls  20737  resspwsds  20960  imasdsf1olem  20961  nmoeq0  21328  idnghm  21335  rrxcph  21909  ovolctb  21986  ovoliunnul  22003  vitalilem4  22105  vitalilem5  22106  ismbf  22122  mbfconst  22127  mbfss  22138  mbfmulc2re  22140  mbfneg  22142  mbfmulc2  22155  itg11  22183  itg2const  22232  itg2mulclem  22238  itg2mulc  22239  itg2monolem1  22242  itg0  22271  itgz  22272  itgvallem3  22277  iblposlem  22283  i1fibl  22299  itgitg1  22300  itgge0  22302  iblconst  22309  itgconst  22310  itgfsum  22318  iblmulc2  22322  itgmulc2lem1  22323  bddmulibl  22330  dvcmulf  22433  dvexp  22441  dvexp2  22442  dvmptid  22445  dvmptc  22446  dvef  22466  rolle  22476  dv11cn  22487  ftc1lem4  22525  ftc2  22530  tdeglem4  22543  ply1nzb  22608  plyconst  22688  plyeq0lem  22692  plypf1  22694  coeeulem  22706  plyco  22723  0dgr  22727  0dgrb  22728  dgrcolem2  22756  dgrco  22757  plyremlem  22785  elqaalem3  22802  iaa  22806  taylply2  22848  itgulm  22888  amgmlem  23436  ftalem7  23469  basellem8  23478  dchrfi  23647  dchrptlem3  23658  bra0  26985  padct  27695  xrge0mulc1cn  28077  esumnul  28196  esum0  28197  esumcvg  28234  ofcc  28254  mbfmcst  28386  sibf0  28459  0rrv  28573  ccatmulgnn0dir  28679  plymul02  28686  plymulx  28688  lgam1  28795  txsconlem  28874  cvmliftphtlem  28951  faclim  29337  ovoliunnfl  30221  voliunnfl  30223  volsupnfl  30224  itg2addnclem  30232  iblmulc2nc  30246  itgmulc2nclem1  30247  itgmulc2nclem2  30248  itgmulc2nc  30249  itgabsnc  30250  bddiblnc  30251  ftc1cnnclem  30254  ftc1anclem3  30258  ftc1anclem5  30260  ftc1anclem7  30262  ftc1anclem8  30263  ftc2nc  30265  repwsmet  30496  rrnequiv  30497  mzpconstmpt  30838  mzpcompact2lem  30849  mendlmod  31310  mendassa  31311  expgrowthi  31406  expgrowth  31408  binomcxplemrat  31423  binomcxplemnotnn0  31429  rnmptc  31616  iblconstmpt  31920  iblempty  31930  itgiccshift  31945  itgperiod  31946  itgsbtaddcnst  31947  stoweidlem21  31969  lindsrng01  33269  aacllem  33550