Metamath Proof Explorer


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 }