This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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