Theorem mptv

Description: Function with universal domain in maps-to notation. (Contributed by NM, 16-Aug-2013)

	Ref	Expression
Assertion	mptv	|- ( x e. _V |-> B ) = { <. x , y >. | y = B }

Proof

Step	Hyp	Ref	Expression
1		df-mpt	|- ( x e. _V |-> B ) = { <. x , y >. | ( x e. _V /\ y = B ) }
2		vex	|- x e. _V
3	2	biantrur	|- ( y = B <-> ( x e. _V /\ y = B ) )
4	3	opabbii	|- { <. x , y >. | y = B } = { <. x , y >. | ( x e. _V /\ y = B ) }
5	1 4	eqtr4i	|- ( x e. _V |-> B ) = { <. x , y >. | y = B }