Description: Operation with universal domain in maps-to notation. (Contributed by NM, 16-Aug-2013)
Ref | Expression | ||
---|---|---|---|
Assertion | mpov | |- ( x e. _V , y e. _V |-> C ) = { <. <. x , y >. , z >. | z = C } |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-mpo | |- ( x e. _V , y e. _V |-> C ) = { <. <. x , y >. , z >. | ( ( x e. _V /\ y e. _V ) /\ z = C ) } |
|
2 | vex | |- x e. _V |
|
3 | vex | |- y e. _V |
|
4 | 2 3 | pm3.2i | |- ( x e. _V /\ y e. _V ) |
5 | 4 | biantrur | |- ( z = C <-> ( ( x e. _V /\ y e. _V ) /\ z = C ) ) |
6 | 5 | oprabbii | |- { <. <. x , y >. , z >. | z = C } = { <. <. x , y >. , z >. | ( ( x e. _V /\ y e. _V ) /\ z = C ) } |
7 | 1 6 | eqtr4i | |- ( x e. _V , y e. _V |-> C ) = { <. <. x , y >. , z >. | z = C } |