Theorem fconstmpt 4769

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 3684	. . . 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 4152	. 2 |- { <. x , y >. | ( x e. A /\ y e. { B } ) } = { <. x , y >. | ( x e. A /\ y = B ) }
4		df-xp 4727	. 2 |- ( A X. { B } ) = { <. x , y >. | ( x e. A /\ y e. { B } ) }
5		df-mpt 4148	. 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 3667   {copab 4145   |-> cmpt 4146   X. cxp 4719

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 2802  df-sn 3673  df-opab 4147  df-mpt 4148  df-xp 4727

This theorem is referenced by:  fconst  5527  fcoconst  5812  fmptsn  5836  fconstmpo  6109  ofc12  6252  caofinvl  6254  xpexgALT  6288  inftonninf  10692  fser0const  10785  prod1dc  12134  pws0g  13521  psrlinv  14685  psr1clfi  14689  mpl0fi  14703  cnmptc  14993  dvexp  15422  dvexp2  15423  dvmptidcn  15425  dvmptccn  15426  dvmptid  15427  dvmptc  15428  dvmptfsum  15436  dvef  15438  elply2  15446  plyconst  15456  plycolemc  15469  nninfall  16521  nninfsellemeqinf  16528  nninfnfiinf  16535  exmidsbthrlem  16536