Step |
Hyp |
Ref |
Expression |
1 |
|
df-opab |
|- { <. x , y >. | x R y } = { z | E. x E. y ( z = <. x , y >. /\ x R y ) } |
2 |
|
df-br |
|- ( x R y <-> <. x , y >. e. R ) |
3 |
|
eleq1 |
|- ( z = <. x , y >. -> ( z e. R <-> <. x , y >. e. R ) ) |
4 |
3
|
biimpar |
|- ( ( z = <. x , y >. /\ <. x , y >. e. R ) -> z e. R ) |
5 |
2 4
|
sylan2b |
|- ( ( z = <. x , y >. /\ x R y ) -> z e. R ) |
6 |
5
|
exlimivv |
|- ( E. x E. y ( z = <. x , y >. /\ x R y ) -> z e. R ) |
7 |
6
|
abssi |
|- { z | E. x E. y ( z = <. x , y >. /\ x R y ) } C_ R |
8 |
1 7
|
eqsstri |
|- { <. x , y >. | x R y } C_ R |