Theorem fconstmpt 4895

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 4011	. . . 4 |- ( y e. { B } <-> y = B )
2	1	anbi2i 699	. . 3 |- ( ( x e. A /\ y e. { B } ) <-> ( x e. A /\ y = B ) )
3	2	opabbii 4486	. 2 |- { <. x , y >. | ( x e. A /\ y e. { B } ) } = { <. x , y >. | ( x e. A /\ y = B ) }
4		df-xp 4857	. 2 |- ( A X. { B } ) = { <. x , y >. | ( x e. A /\ y e. { B } ) }
5		df-mpt 4482	. 2 |- ( x e. A |-> B ) = { <. x , y >. | ( x e. A /\ y = B ) }
6	3, 4, 5	3eqtr4i 2462	1 |- ( A X. { B } ) = ( x e. A |-> B )

Syntax hints:   /\ wa 371   = wceq 1438   e. wcel 1869   {csn 3997   {copab 4479   |-> cmpt 4480   X. cxp 4849

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-5 1749  ax-6 1795  ax-7 1840  ax-10 1888  ax-11 1893  ax-12 1906  ax-13 2054  ax-ext 2401

This theorem depends on definitions:  df-bi 189  df-an 373  df-tru 1441  df-ex 1661  df-nf 1665  df-sb 1788  df-clab 2409  df-cleq 2415  df-clel 2418  df-sn 3998  df-opab 4481  df-mpt 4482  df-xp 4857

This theorem is referenced by:  fconst  5784  fcoconst  6073  fmptsn  6097  fconstmpt2  6403  ofc12  6568  caofinvl  6570  xpexgALT  6798  cantnf  8201  cnfcom2lem  8209  repsconst  12871  harmonic  13910  geomulcvg  13925  vdwlem8  14931  ramcl  14980  pwsvscafval  15385  setcepi  15976  diag2  16123  pws0g  16565  0frgp  17422  pwsgsum  17604  lmhmvsca  18261  rrgsupp  18508  psrlinv  18614  psrlidm  18620  psrridm  18621  psrass23l  18625  psrass23  18627  mplcoe1  18682  mplcoe3  18683  mplcoe5  18685  mplmon2  18709  evlslem2  18728  evlslem1  18731  coe1z  18849  coe1mul2lem1  18853  coe1tm  18859  coe1sclmul  18868  coe1sclmul2  18870  evls1sca  18905  evl1sca  18915  uvcresum  19343  grpvrinv  19413  mdetunilem9  19637  pttoponconst  20604  cnmptc  20669  cnmptkc  20686  pt1hmeo  20813  tmdgsum2  21103  tsms0  21148  tgptsmscls  21156  resspwsds  21379  imasdsf1olem  21380  nmoeq0  21749  idnghm  21756  rrxcph  22343  ovolctb  22435  ovoliunnul  22452  vitalilem4  22561  vitalilem5  22562  ismbf  22578  mbfconst  22583  mbfss  22594  mbfmulc2re  22596  mbfneg  22598  mbfmulc2  22611  itg11  22641  itg2const  22690  itg2mulclem  22696  itg2mulc  22697  itg2monolem1  22700  itg0  22729  itgz  22730  itgvallem3  22735  iblposlem  22741  i1fibl  22757  itgitg1  22758  itgge0  22760  iblconst  22767  itgconst  22768  itgfsum  22776  iblmulc2  22780  itgmulc2lem1  22781  bddmulibl  22788  dvcmulf  22891  dvexp  22899  dvexp2  22900  dvmptid  22903  dvmptc  22904  dvef  22924  rolle  22934  dv11cn  22945  ftc1lem4  22983  ftc2  22988  tdeglem4  23001  ply1nzb  23063  plyconst  23152  plyeq0lem  23156  plypf1  23158  coeeulem  23170  plyco  23187  0dgr  23191  0dgrb  23192  dgrcolem2  23220  dgrco  23221  plyremlem  23249  elqaalem3  23266  elqaalem3OLD  23269  iaa  23273  taylply2  23315  itgulm  23355  amgmlem  23907  lgam1  23981  ftalem7  23997  basellem8  24006  dchrfi  24175  dchrptlem3  24186  bra0  27595  padct  28307  xrge0mulc1cn  28749  esumnul  28871  esum0  28872  esumcvg  28909  ofcc  28929  mbfmcst  29083  sibf0  29169  0rrv  29286  ccatmulgnn0dir  29430  plymul02  29437  plymulx  29439  txsconlem  29965  cvmliftphtlem  30042  faclim  30383  poimirlem30  31928  ovoliunnfl  31940  voliunnfl  31942  volsupnfl  31943  itg2addnclem  31951  iblmulc2nc  31965  itgmulc2nclem1  31966  itgmulc2nclem2  31967  itgmulc2nc  31968  itgabsnc  31969  bddiblnc  31970  ftc1cnnclem  31973  ftc1anclem3  31977  ftc1anclem5  31979  ftc1anclem7  31981  ftc1anclem8  31982  ftc2nc  31984  repwsmet  32124  rrnequiv  32125  mzpconstmpt  35545  mzpcompact2lem  35556  mendlmod  36023  mendassa  36024  expgrowthi  36584  expgrowth  36586  binomcxplemrat  36601  binomcxplemnotnn0  36607  rnmptc  37330  iblconstmpt  37696  iblempty  37706  itgiccshift  37721  itgperiod  37722  itgsbtaddcnst  37723  stoweidlem21  37745  lindsrng01  39605  aacllem  39884