Step |
Hyp |
Ref |
Expression |
1 |
|
resubval |
|- ( ( x e. RR /\ y e. RR ) -> ( x -R y ) = ( iota_ z e. RR ( y + z ) = x ) ) |
2 |
|
rersubcl |
|- ( ( x e. RR /\ y e. RR ) -> ( x -R y ) e. RR ) |
3 |
1 2
|
eqeltrrd |
|- ( ( x e. RR /\ y e. RR ) -> ( iota_ z e. RR ( y + z ) = x ) e. RR ) |
4 |
3
|
rgen2 |
|- A. x e. RR A. y e. RR ( iota_ z e. RR ( y + z ) = x ) e. RR |
5 |
|
df-resub |
|- -R = ( x e. RR , y e. RR |-> ( iota_ z e. RR ( y + z ) = x ) ) |
6 |
5
|
fmpo |
|- ( A. x e. RR A. y e. RR ( iota_ z e. RR ( y + z ) = x ) e. RR <-> -R : ( RR X. RR ) --> RR ) |
7 |
4 6
|
mpbi |
|- -R : ( RR X. RR ) --> RR |