Step |
Hyp |
Ref |
Expression |
1 |
|
ovid.1 |
|- ( ( x e. R /\ y e. S ) -> E! z ph ) |
2 |
|
ovid.2 |
|- F = { <. <. x , y >. , z >. | ( ( x e. R /\ y e. S ) /\ ph ) } |
3 |
|
df-ov |
|- ( x F y ) = ( F ` <. x , y >. ) |
4 |
3
|
eqeq1i |
|- ( ( x F y ) = z <-> ( F ` <. x , y >. ) = z ) |
5 |
1
|
fnoprab |
|- { <. <. x , y >. , z >. | ( ( x e. R /\ y e. S ) /\ ph ) } Fn { <. x , y >. | ( x e. R /\ y e. S ) } |
6 |
2
|
fneq1i |
|- ( F Fn { <. x , y >. | ( x e. R /\ y e. S ) } <-> { <. <. x , y >. , z >. | ( ( x e. R /\ y e. S ) /\ ph ) } Fn { <. x , y >. | ( x e. R /\ y e. S ) } ) |
7 |
5 6
|
mpbir |
|- F Fn { <. x , y >. | ( x e. R /\ y e. S ) } |
8 |
|
opabidw |
|- ( <. x , y >. e. { <. x , y >. | ( x e. R /\ y e. S ) } <-> ( x e. R /\ y e. S ) ) |
9 |
8
|
biimpri |
|- ( ( x e. R /\ y e. S ) -> <. x , y >. e. { <. x , y >. | ( x e. R /\ y e. S ) } ) |
10 |
|
fnopfvb |
|- ( ( F Fn { <. x , y >. | ( x e. R /\ y e. S ) } /\ <. x , y >. e. { <. x , y >. | ( x e. R /\ y e. S ) } ) -> ( ( F ` <. x , y >. ) = z <-> <. <. x , y >. , z >. e. F ) ) |
11 |
7 9 10
|
sylancr |
|- ( ( x e. R /\ y e. S ) -> ( ( F ` <. x , y >. ) = z <-> <. <. x , y >. , z >. e. F ) ) |
12 |
2
|
eleq2i |
|- ( <. <. x , y >. , z >. e. F <-> <. <. x , y >. , z >. e. { <. <. x , y >. , z >. | ( ( x e. R /\ y e. S ) /\ ph ) } ) |
13 |
|
oprabidw |
|- ( <. <. x , y >. , z >. e. { <. <. x , y >. , z >. | ( ( x e. R /\ y e. S ) /\ ph ) } <-> ( ( x e. R /\ y e. S ) /\ ph ) ) |
14 |
12 13
|
bitri |
|- ( <. <. x , y >. , z >. e. F <-> ( ( x e. R /\ y e. S ) /\ ph ) ) |
15 |
14
|
baib |
|- ( ( x e. R /\ y e. S ) -> ( <. <. x , y >. , z >. e. F <-> ph ) ) |
16 |
11 15
|
bitrd |
|- ( ( x e. R /\ y e. S ) -> ( ( F ` <. x , y >. ) = z <-> ph ) ) |
17 |
4 16
|
bitrid |
|- ( ( x e. R /\ y e. S ) -> ( ( x F y ) = z <-> ph ) ) |