Theorem fconstmpt 4878

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 3888	. . . 4 |- ( y e. { B } <-> y = B )
2	1	anbi2i 689	. . 3 |- ( ( x e. A /\ y e. { B } ) <-> ( x e. A /\ y = B ) )
3	2	opabbii 4353	. 2 |- { <. x , y >. | ( x e. A /\ y e. { B } ) } = { <. x , y >. | ( x e. A /\ y = B ) }
4		df-xp 4842	. 2 |- ( A X. { B } ) = { <. x , y >. | ( x e. A /\ y e. { B } ) }
5		df-mpt 4349	. 2 |- ( x e. A |-> B ) = { <. x , y >. | ( x e. A /\ y = B ) }
6	3, 4, 5	3eqtr4i 2471	1 |- ( A X. { B } ) = ( x e. A |-> B )

Syntax hints:   /\ wa 369   = wceq 1364   e. wcel 1761   {csn 3874   {copab 4346   e. cmpt 4347   X. cxp 4834

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1706  df-clab 2428  df-cleq 2434  df-clel 2437  df-sn 3875  df-opab 4348  df-mpt 4349  df-xp 4842

This theorem is referenced by:  fconst  5593  fcoconst  5877  fmptsn  5896  fconstmpt2  6184  ofc12  6344  caofinvl  6346  xpexgALT  6569  cantnf  7897  cantnfOLD  7919  cnfcom2lem  7930  cnfcom2lemOLD  7938  repsconst  12406  harmonic  13317  geomulcvg  13332  vdwlem8  14045  ramcl  14086  pwsvscafval  14428  setcepi  14952  diag2  15051  pws0g  15453  0frgp  16269  pwsgsum  16463  pwsgsumOLD  16464  lmhmvsca  17104  rrgsupp  17340  rrgsuppOLD  17341  psrlinv  17446  psrlidm  17452  psrridm  17454  psrass23  17460  mplcoe1  17522  mplcoe3  17523  mplcoe3OLD  17524  mplcoe2  17525  mplcoe2OLD  17526  mplmon2  17551  evlslem2  17573  evlslem1  17577  coe1z  17692  coe1mul2lem1  17696  coe1tm  17701  coe1sclmul  17710  coe1sclmul2  17712  evls1sca  17731  evl1sca  17737  uvcresum  18177  grpvrinv  18255  mdetunilem9  18385  pttoponconst  19129  cnmptc  19194  cnmptkc  19211  pt1hmeo  19338  tmdgsum2  19626  tsms0  19674  tgptsmscls  19683  resspwsds  19906  imasdsf1olem  19907  nmoeq0  20274  idnghm  20281  rrxcph  20855  ovolctb  20932  ovoliunnul  20949  vitalilem4  21050  vitalilem5  21051  ismbf  21067  mbfconst  21072  mbfss  21083  mbfmulc2re  21085  mbfneg  21087  mbfmulc2  21100  itg11  21128  itg2const  21177  itg2mulclem  21183  itg2mulc  21184  itg2monolem1  21187  itg0  21216  itgz  21217  itgvallem3  21222  iblposlem  21228  i1fibl  21244  itgitg1  21245  itgge0  21247  iblconst  21254  itgconst  21255  itgfsum  21263  iblmulc2  21267  itgmulc2lem1  21268  bddmulibl  21275  dvcmulf  21378  dvexp  21386  dvexp2  21387  dvmptid  21390  dvmptc  21391  dvef  21411  rolle  21421  dv11cn  21432  ftc1lem4  21470  ftc2  21475  tdeglem4  21488  ply1nzb  21553  plyconst  21633  plyeq0lem  21637  plypf1  21639  coeeulem  21651  plyco  21668  0dgr  21672  0dgrb  21673  dgrcolem2  21700  dgrco  21701  plyremlem  21729  elqaalem3  21746  iaa  21750  taylply2  21792  itgulm  21832  amgmlem  22342  ftalem7  22375  basellem8  22384  dchrfi  22553  dchrptlem3  22564  bra0  25289  xrge0mulc1cn  26307  esumnul  26438  esum0  26439  esumcvg  26471  ofcc  26484  mbfmcst  26610  sibf0  26650  0rrv  26764  ccatmulgnn0dir  26870  plymul02  26877  plymulx  26879  lgam1  26980  txsconlem  27059  cvmliftphtlem  27136  faclim  27481  ovoliunnfl  28358  voliunnfl  28360  volsupnfl  28361  itg2addnclem  28368  iblmulc2nc  28382  itgmulc2nclem1  28383  itgmulc2nclem2  28384  itgmulc2nc  28385  itgabsnc  28386  bddiblnc  28387  ftc1cnnclem  28390  ftc1anclem3  28394  ftc1anclem5  28396  ftc1anclem7  28398  ftc1anclem8  28399  ftc2nc  28401  repwsmet  28658  rrnequiv  28659  mzpconstmpt  29001  mzpcompact2lem  29013  mendlmod  29475  mendassa  29476  expgrowthi  29532  expgrowth  29534  stoweidlem21  29741  psrass23l  30725  lindsrng01  30843