Theorem fconstmpt 5163

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		velsn 4193	. . . 4 |- ( y e. { B } <-> y = B )
2	1	anbi2i 730	. . 3 |- ( ( x e. A /\ y e. { B } ) <-> ( x e. A /\ y = B ) )
3	2	opabbii 4717	. 2 |- { <. x , y >. | ( x e. A /\ y e. { B } ) } = { <. x , y >. | ( x e. A /\ y = B ) }
4		df-xp 5120	. 2 |- ( A X. { B } ) = { <. x , y >. | ( x e. A /\ y e. { B } ) }
5		df-mpt 4730	. 2 |- ( x e. A |-> B ) = { <. x , y >. | ( x e. A /\ y = B ) }
6	3, 4, 5	3eqtr4i 2654	1 |- ( A X. { B } ) = ( x e. A |-> B )

Syntax hints:   /\ wa 384   = wceq 1483   e. wcel 1990   {csn 4177   {copab 4712   |-> cmpt 4729   X. cxp 5112

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-sn 4178  df-opab 4713  df-mpt 4730  df-xp 5120

This theorem is referenced by:  fconst  6091  fcoconst  6401  fmptsn  6433  fconstmpt2  6755  ofc12  6922  caofinvl  6924  xpexgALT  7161  cantnf  8590  cnfcom2lem  8598  repsconst  13519  harmonic  14591  geomulcvg  14607  vdwlem8  15692  ramcl  15733  pwsvscafval  16154  setcepi  16738  diag2  16885  pws0g  17326  0frgp  18192  pwsgsum  18378  lmhmvsca  19045  rrgsupp  19291  psrlinv  19397  psrlidm  19403  psrridm  19404  psrass23l  19408  psrass23  19410  mplcoe1  19465  mplcoe3  19466  mplcoe5  19468  mplmon2  19493  evlslem2  19512  evlslem1  19515  coe1z  19633  coe1mul2lem1  19637  coe1tm  19643  coe1sclmul  19652  coe1sclmul2  19654  evls1sca  19688  evl1sca  19698  uvcresum  20132  grpvrinv  20202  mdetunilem9  20426  pttoponconst  21400  cnmptc  21465  cnmptkc  21482  pt1hmeo  21609  tmdgsum2  21900  tsms0  21945  tgptsmscls  21953  resspwsds  22177  imasdsf1olem  22178  nmoeq0  22540  idnghm  22547  rrxcph  23180  ovolctb  23258  ovoliunnul  23275  vitalilem4  23380  vitalilem5  23381  ismbf  23397  mbfconst  23402  mbfss  23413  mbfmulc2re  23415  mbfneg  23417  mbfmulc2  23430  itg11  23458  itg2const  23507  itg2mulclem  23513  itg2mulc  23514  itg2monolem1  23517  itg0  23546  itgz  23547  itgvallem3  23552  iblposlem  23558  i1fibl  23574  itgitg1  23575  itgge0  23577  iblconst  23584  itgconst  23585  itgfsum  23593  iblmulc2  23597  itgmulc2lem1  23598  bddmulibl  23605  dvcmulf  23708  dvexp  23716  dvexp2  23717  dvmptid  23720  dvmptc  23721  dvef  23743  rolle  23753  dv11cn  23764  ftc1lem4  23802  ftc2  23807  tdeglem4  23820  ply1nzb  23882  plyconst  23962  plyeq0lem  23966  plypf1  23968  coeeulem  23980  plyco  23997  0dgr  24001  0dgrb  24002  dgrcolem2  24030  dgrco  24031  plyremlem  24059  elqaalem3  24076  iaa  24080  taylply2  24122  itgulm  24162  amgmlem  24716  lgam1  24790  ftalem7  24805  basellem8  24814  dchrfi  24980  dchrptlem3  24991  bra0  28809  padct  29497  xrge0mulc1cn  29987  esumnul  30110  esum0  30111  esumcvg  30148  ofcc  30168  mbfmcst  30321  sibf0  30396  0rrv  30513  ccatmulgnn0dir  30619  plymul02  30623  plymulx  30625  txsconnlem  31222  cvmliftphtlem  31299  faclim  31632  matunitlindflem1  33405  poimirlem30  33439  ovoliunnfl  33451  voliunnfl  33453  volsupnfl  33454  itg2addnclem  33461  iblmulc2nc  33475  itgmulc2nclem1  33476  itgmulc2nclem2  33477  itgmulc2nc  33478  itgabsnc  33479  bddiblnc  33480  ftc1cnnclem  33483  ftc1anclem3  33487  ftc1anclem5  33489  ftc1anclem7  33491  ftc1anclem8  33492  ftc2nc  33494  repwsmet  33633  rrnequiv  33634  mzpconstmpt  37303  mzpcompact2lem  37314  mendlmod  37763  mendassa  37764  expgrowthi  38532  expgrowth  38534  binomcxplemrat  38549  binomcxplemnotnn0  38555  rnmptc  39353  climconstmpt  39890  iblconstmpt  40171  iblempty  40181  itgiccshift  40196  itgperiod  40197  itgsbtaddcnst  40198  stoweidlem21  40238  lindsrng01  42257  aacllem  42547  amgmlemALT  42549