Theorem fconstmpt 4763

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 3683	. . . 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 4150	. 2 |- { <. x , y >. | ( x e. A /\ y e. { B } ) } = { <. x , y >. | ( x e. A /\ y = B ) }
4		df-xp 4722	. 2 |- ( A X. { B } ) = { <. x , y >. | ( x e. A /\ y e. { B } ) }
5		df-mpt 4146	. 2 |- ( x e. A |-> B ) = { <. x , y >. | ( x e. A /\ y = B ) }
6	3, 4, 5	3eqtr4i 2260	1 |- ( A X. { B } ) = ( x e. A |-> B )

Syntax hints:   /\ wa 104   = wceq 1395   e. wcel 2200   {csn 3666   {copab 4143   |-> cmpt 4144   X. cxp 4714

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-v 2801  df-sn 3672  df-opab 4145  df-mpt 4146  df-xp 4722

This theorem is referenced by:  fconst  5517  fcoconst  5799  fmptsn  5821  fconstmpo  6090  ofc12  6232  caofinvl  6234  xpexgALT  6268  inftonninf  10651  fser0const  10744  prod1dc  12083  pws0g  13470  psrlinv  14633  psr1clfi  14637  mpl0fi  14651  cnmptc  14941  dvexp  15370  dvexp2  15371  dvmptidcn  15373  dvmptccn  15374  dvmptid  15375  dvmptc  15376  dvmptfsum  15384  dvef  15386  elply2  15394  plyconst  15404  plycolemc  15417  nninfall  16306  nninfsellemeqinf  16313  nninfnfiinf  16320  exmidsbthrlem  16321