Metamath Proof Explorer


Theorem sqrt11i

Description: The square root function is one-to-one. (Contributed by NM, 27-Jul-1999)

Ref Expression
Hypotheses sqrtthi.1
|- A e. RR
sqr11.1
|- B e. RR
Assertion sqrt11i
|- ( ( 0 <_ A /\ 0 <_ B ) -> ( ( sqrt ` A ) = ( sqrt ` B ) <-> A = B ) )

Proof

Step Hyp Ref Expression
1 sqrtthi.1
 |-  A e. RR
2 sqr11.1
 |-  B e. RR
3 sqrt11
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> ( ( sqrt ` A ) = ( sqrt ` B ) <-> A = B ) )
4 2 3 mpanr1
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ 0 <_ B ) -> ( ( sqrt ` A ) = ( sqrt ` B ) <-> A = B ) )
5 1 4 mpanl1
 |-  ( ( 0 <_ A /\ 0 <_ B ) -> ( ( sqrt ` A ) = ( sqrt ` B ) <-> A = B ) )