Theorem fconstmpt 5042

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 4041	. . . 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 4511	. 2 |- { <. x , y >. | ( x e. A /\ y e. { B } ) } = { <. x , y >. | ( x e. A /\ y = B ) }
4		df-xp 5005	. 2 |- ( A X. { B } ) = { <. x , y >. | ( x e. A /\ y e. { B } ) }
5		df-mpt 4507	. 2 |- ( x e. A |-> B ) = { <. x , y >. | ( x e. A /\ y = B ) }
6	3, 4, 5	3eqtr4i 2506	1 |- ( A X. { B } ) = ( x e. A |-> B )

Syntax hints:   /\ wa 369   = wceq 1379   e. wcel 1767   {csn 4027   {copab 4504   |-> cmpt 4505   X. cxp 4997

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-sn 4028  df-opab 4506  df-mpt 4507  df-xp 5005

This theorem is referenced by:  fconst  5770  fcoconst  6057  fmptsn  6080  fconstmpt2  6380  ofc12  6548  caofinvl  6550  xpexgALT  6777  cantnf  8111  cantnfOLD  8133  cnfcom2lem  8144  cnfcom2lemOLD  8152  repsconst  12706  harmonic  13632  geomulcvg  13647  vdwlem8  14364  ramcl  14405  pwsvscafval  14748  setcepi  15272  diag2  15371  pws0g  15774  0frgp  16600  pwsgsum  16809  pwsgsumOLD  16810  lmhmvsca  17486  rrgsupp  17726  rrgsuppOLD  17727  psrlinv  17837  psrlidm  17843  psrridm  17845  psrass23l  17850  psrass23  17852  mplcoe1  17914  mplcoe3  17915  mplcoe3OLD  17916  mplcoe5  17918  mplcoe2OLD  17920  mplmon2  17945  evlslem2  17967  evlslem1  17971  coe1z  18091  coe1mul2lem1  18095  coe1tm  18101  coe1sclmul  18110  coe1sclmul2  18112  evls1sca  18147  evl1sca  18157  uvcresum  18607  grpvrinv  18681  mdetunilem9  18905  pttoponconst  19849  cnmptc  19914  cnmptkc  19931  pt1hmeo  20058  tmdgsum2  20346  tsms0  20394  tgptsmscls  20403  resspwsds  20626  imasdsf1olem  20627  nmoeq0  20994  idnghm  21001  rrxcph  21575  ovolctb  21652  ovoliunnul  21669  vitalilem4  21771  vitalilem5  21772  ismbf  21788  mbfconst  21793  mbfss  21804  mbfmulc2re  21806  mbfneg  21808  mbfmulc2  21821  itg11  21849  itg2const  21898  itg2mulclem  21904  itg2mulc  21905  itg2monolem1  21908  itg0  21937  itgz  21938  itgvallem3  21943  iblposlem  21949  i1fibl  21965  itgitg1  21966  itgge0  21968  iblconst  21975  itgconst  21976  itgfsum  21984  iblmulc2  21988  itgmulc2lem1  21989  bddmulibl  21996  dvcmulf  22099  dvexp  22107  dvexp2  22108  dvmptid  22111  dvmptc  22112  dvef  22132  rolle  22142  dv11cn  22153  ftc1lem4  22191  ftc2  22196  tdeglem4  22209  ply1nzb  22274  plyconst  22354  plyeq0lem  22358  plypf1  22360  coeeulem  22372  plyco  22389  0dgr  22393  0dgrb  22394  dgrcolem2  22421  dgrco  22422  plyremlem  22450  elqaalem3  22467  iaa  22471  taylply2  22513  itgulm  22553  amgmlem  23063  ftalem7  23096  basellem8  23105  dchrfi  23274  dchrptlem3  23285  bra0  26561  xrge0mulc1cn  27575  esumnul  27715  esum0  27716  esumcvg  27748  ofcc  27761  mbfmcst  27886  sibf0  27932  0rrv  28046  ccatmulgnn0dir  28152  plymul02  28159  plymulx  28161  lgam1  28262  txsconlem  28341  cvmliftphtlem  28418  faclim  28764  ovoliunnfl  29649  voliunnfl  29651  volsupnfl  29652  itg2addnclem  29659  iblmulc2nc  29673  itgmulc2nclem1  29674  itgmulc2nclem2  29675  itgmulc2nc  29676  itgabsnc  29677  bddiblnc  29678  ftc1cnnclem  29681  ftc1anclem3  29685  ftc1anclem5  29687  ftc1anclem7  29689  ftc1anclem8  29690  ftc2nc  29692  repwsmet  29949  rrnequiv  29950  mzpconstmpt  30292  mzpcompact2lem  30304  mendlmod  30763  mendassa  30764  expgrowthi  30854  expgrowth  30856  rnmptc  31043  iblconstmpt  31289  iblempty  31299  itgiccshift  31314  itgperiod  31315  itgsbtaddcnst  31316  stoweidlem21  31337  lindsrng01  32159