Step |
Hyp |
Ref |
Expression |
1 |
|
xpsff1o.f |
|- F = ( x e. A , y e. B |-> { <. (/) , x >. , <. 1o , y >. } ) |
2 |
|
simpl |
|- ( ( x = X /\ y = Y ) -> x = X ) |
3 |
2
|
opeq2d |
|- ( ( x = X /\ y = Y ) -> <. (/) , x >. = <. (/) , X >. ) |
4 |
|
simpr |
|- ( ( x = X /\ y = Y ) -> y = Y ) |
5 |
4
|
opeq2d |
|- ( ( x = X /\ y = Y ) -> <. 1o , y >. = <. 1o , Y >. ) |
6 |
3 5
|
preq12d |
|- ( ( x = X /\ y = Y ) -> { <. (/) , x >. , <. 1o , y >. } = { <. (/) , X >. , <. 1o , Y >. } ) |
7 |
|
prex |
|- { <. (/) , X >. , <. 1o , Y >. } e. _V |
8 |
6 1 7
|
ovmpoa |
|- ( ( X e. A /\ Y e. B ) -> ( X F Y ) = { <. (/) , X >. , <. 1o , Y >. } ) |