Theorem fconstmpt 5033

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 4028	. . . 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 4501	. 2 |- { <. x , y >. | ( x e. A /\ y e. { B } ) } = { <. x , y >. | ( x e. A /\ y = B ) }
4		df-xp 4995	. 2 |- ( A X. { B } ) = { <. x , y >. | ( x e. A /\ y e. { B } ) }
5		df-mpt 4497	. 2 |- ( x e. A |-> B ) = { <. x , y >. | ( x e. A /\ y = B ) }
6	3, 4, 5	3eqtr4i 2482	1 |- ( A X. { B } ) = ( x e. A |-> B )

Syntax hints:   /\ wa 369   = wceq 1383   e. wcel 1804   {csn 4014   {copab 4494   |-> cmpt 4495   X. cxp 4987

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-sn 4015  df-opab 4496  df-mpt 4497  df-xp 4995

This theorem is referenced by:  fconst  5761  fcoconst  6053  fmptsn  6076  fconstmpt2  6382  ofc12  6550  caofinvl  6552  xpexgALT  6778  cantnf  8115  cantnfOLD  8137  cnfcom2lem  8148  cnfcom2lemOLD  8156  repsconst  12726  harmonic  13652  geomulcvg  13667  vdwlem8  14488  ramcl  14529  pwsvscafval  14873  setcepi  15394  diag2  15493  pws0g  15935  0frgp  16776  pwsgsum  16988  pwsgsumOLD  16989  lmhmvsca  17670  rrgsupp  17918  rrgsuppOLD  17919  psrlinv  18029  psrlidm  18035  psrridm  18037  psrass23l  18042  psrass23  18044  mplcoe1  18106  mplcoe3  18107  mplcoe3OLD  18108  mplcoe5  18110  mplcoe2OLD  18112  mplmon2  18137  evlslem2  18159  evlslem1  18163  coe1z  18283  coe1mul2lem1  18287  coe1tm  18293  coe1sclmul  18302  coe1sclmul2  18304  evls1sca  18339  evl1sca  18349  uvcresum  18802  grpvrinv  18876  mdetunilem9  19100  pttoponconst  20076  cnmptc  20141  cnmptkc  20158  pt1hmeo  20285  tmdgsum2  20573  tsms0  20621  tgptsmscls  20630  resspwsds  20853  imasdsf1olem  20854  nmoeq0  21221  idnghm  21228  rrxcph  21802  ovolctb  21879  ovoliunnul  21896  vitalilem4  21998  vitalilem5  21999  ismbf  22015  mbfconst  22020  mbfss  22031  mbfmulc2re  22033  mbfneg  22035  mbfmulc2  22048  itg11  22076  itg2const  22125  itg2mulclem  22131  itg2mulc  22132  itg2monolem1  22135  itg0  22164  itgz  22165  itgvallem3  22170  iblposlem  22176  i1fibl  22192  itgitg1  22193  itgge0  22195  iblconst  22202  itgconst  22203  itgfsum  22211  iblmulc2  22215  itgmulc2lem1  22216  bddmulibl  22223  dvcmulf  22326  dvexp  22334  dvexp2  22335  dvmptid  22338  dvmptc  22339  dvef  22359  rolle  22369  dv11cn  22380  ftc1lem4  22418  ftc2  22423  tdeglem4  22436  ply1nzb  22501  plyconst  22581  plyeq0lem  22585  plypf1  22587  coeeulem  22599  plyco  22616  0dgr  22620  0dgrb  22621  dgrcolem2  22649  dgrco  22650  plyremlem  22678  elqaalem3  22695  iaa  22699  taylply2  22741  itgulm  22781  amgmlem  23297  ftalem7  23330  basellem8  23339  dchrfi  23508  dchrptlem3  23519  bra0  26847  xrge0mulc1cn  27901  esumnul  28037  esum0  28038  esumcvg  28070  ofcc  28083  mbfmcst  28208  sibf0  28254  0rrv  28368  ccatmulgnn0dir  28474  plymul02  28481  plymulx  28483  lgam1  28584  txsconlem  28663  cvmliftphtlem  28740  faclim  29147  ovoliunnfl  30032  voliunnfl  30034  volsupnfl  30035  itg2addnclem  30042  iblmulc2nc  30056  itgmulc2nclem1  30057  itgmulc2nclem2  30058  itgmulc2nc  30059  itgabsnc  30060  bddiblnc  30061  ftc1cnnclem  30064  ftc1anclem3  30068  ftc1anclem5  30070  ftc1anclem7  30072  ftc1anclem8  30073  ftc2nc  30075  repwsmet  30306  rrnequiv  30307  mzpconstmpt  30648  mzpcompact2lem  30660  mendlmod  31118  mendassa  31119  expgrowthi  31214  expgrowth  31216  rnmptc  31403  iblconstmpt  31708  iblempty  31718  itgiccshift  31733  itgperiod  31734  itgsbtaddcnst  31735  stoweidlem21  31757  lindsrng01  32939