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 } |
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 } |