Theorem fconstmpt 4779

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 3690	. . . 4 |- ( y e. { B } <-> y = B )
2	1	anbi2i 457	. . 3 |- ( ( x e. A /\ y e. { B } ) <-> ( x e. A /\ y = B ) )
3	2	opabbii 4161	. 2 |- { <. x , y >. | ( x e. A /\ y e. { B } ) } = { <. x , y >. | ( x e. A /\ y = B ) }
4		df-xp 4737	. 2 |- ( A X. { B } ) = { <. x , y >. | ( x e. A /\ y e. { B } ) }
5		df-mpt 4157	. 2 |- ( x e. A |-> B ) = { <. x , y >. | ( x e. A /\ y = B ) }
6	3, 4, 5	3eqtr4i 2262	1 |- ( A X. { B } ) = ( x e. A |-> B )

Syntax hints:   /\ wa 104   = wceq 1398   e. wcel 2202   {csn 3673   {copab 4154   |-> cmpt 4155   X. cxp 4729

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-v 2805  df-sn 3679  df-opab 4156  df-mpt 4157  df-xp 4737

This theorem is referenced by:  fconst  5541  fcoconst  5826  fmptsn  5851  fconstmpo  6126  ofc12  6268  caofinvl  6270  xpexgALT  6304  inftonninf  10750  fser0const  10843  prod1dc  12210  pws0g  13597  rrgsupp  14344  psrlinv  14768  psr1clfi  14772  mpl0fi  14786  cnmptc  15076  dvexp  15505  dvexp2  15506  dvmptidcn  15508  dvmptccn  15509  dvmptid  15510  dvmptc  15511  dvmptfsum  15519  dvef  15521  elply2  15529  plyconst  15539  plycolemc  15552  nninfall  16718  nninfsellemeqinf  16725  nninfnfiinf  16732  exmidsbthrlem  16733