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 𝐴 ∈ ℝ
sqr11.1 𝐵 ∈ ℝ
Assertion sqrt11i ( ( 0 ≤ 𝐴 ∧ 0 ≤ 𝐵 ) → ( ( √ ‘ 𝐴 ) = ( √ ‘ 𝐵 ) ↔ 𝐴 = 𝐵 ) )

Proof

Step Hyp Ref Expression
1 sqrtthi.1 𝐴 ∈ ℝ
2 sqr11.1 𝐵 ∈ ℝ
3 sqrt11 ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ) → ( ( √ ‘ 𝐴 ) = ( √ ‘ 𝐵 ) ↔ 𝐴 = 𝐵 ) )
4 2 3 mpanr1 ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 0 ≤ 𝐵 ) → ( ( √ ‘ 𝐴 ) = ( √ ‘ 𝐵 ) ↔ 𝐴 = 𝐵 ) )
5 1 4 mpanl1 ( ( 0 ≤ 𝐴 ∧ 0 ≤ 𝐵 ) → ( ( √ ‘ 𝐴 ) = ( √ ‘ 𝐵 ) ↔ 𝐴 = 𝐵 ) )