Metamath Proof Explorer

Theorem repncan2

Description: Addition and subtraction of equals. Compare pncan2 . (Contributed by Steven Nguyen, 8-Jan-2023)

Ref Expression
Assertion repncan2 
|- ( ( A e. RR /\ B e. RR ) -> ( ( A + B ) -R A ) = B )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( A + B ) = ( A + B )
2 readdcl 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A + B ) e. RR )
3 simpl 
 |-  ( ( A e. RR /\ B e. RR ) -> A e. RR )
4 simpr 
 |-  ( ( A e. RR /\ B e. RR ) -> B e. RR )
5 2 3 4 resubaddd 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( ( A + B ) -R A ) = B <-> ( A + B ) = ( A + B ) ) )
6 1 5 mpbiri 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( A + B ) -R A ) = B )