Theorem dfmpt

Description: Alternate definition for the maps-to notation df-mpt (although it requires that B be a set). (Contributed by NM, 24-Aug-2010) (Revised by Mario Carneiro, 30-Dec-2016)

	Ref	Expression
Hypothesis	dfmpt.1	|- B e. _V
Assertion	dfmpt	|- ( x e. A |-> B ) = U_ x e. A { <. x , B >. }

Proof

Step	Hyp	Ref	Expression
1		dfmpt.1	|- B e. _V
2		dfmpt3	|- ( x e. A |-> B ) = U_ x e. A ( { x } X. { B } )
3		vex	|- x e. _V
4	3 1	xpsn	|- ( { x } X. { B } ) = { <. x , B >. }
5	4	a1i	|- ( x e. A -> ( { x } X. { B } ) = { <. x , B >. } )
6	5	iuneq2i	|- U_ x e. A ( { x } X. { B } ) = U_ x e. A { <. x , B >. }
7	2 6	eqtri	|- ( x e. A |-> B ) = U_ x e. A { <. x , B >. }