Theorem fconstmpt

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)

	Ref	Expression
Assertion	fconstmpt	|- ( A X. { B } ) = ( x e. A |-> B )

Proof

Step	Hyp	Ref	Expression
1		velsn	|- ( y e. { B } <-> y = B )
2	1	anbi2i	|- ( ( x e. A /\ y e. { B } ) <-> ( x e. A /\ y = B ) )
3	2	opabbii	|- { <. x , y >. | ( x e. A /\ y e. { B } ) } = { <. x , y >. | ( x e. A /\ y = B ) }
4		df-xp	|- ( A X. { B } ) = { <. x , y >. | ( x e. A /\ y e. { B } ) }
5		df-mpt	|- ( x e. A |-> B ) = { <. x , y >. | ( x e. A /\ y = B ) }
6	3 4 5	3eqtr4i	|- ( A X. { B } ) = ( x e. A |-> B )