Metamath Proof Explorer


Theorem resubf

Description: Real subtraction is an operation on the real numbers. Based on subf . (Contributed by Steven Nguyen, 7-Jan-2023)

Ref Expression
Assertion resubf
|- -R : ( RR X. RR ) --> RR

Proof

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