Theorem eqresr

Description: Equality of real numbers in terms of intermediate signed reals. (Contributed by NM, 10-May-1996) (New usage is discouraged.)

	Ref	Expression
Hypothesis	eqresr.1	⊢ 𝐴 ∈ V
Assertion	eqresr	⊢ ( ⟨ 𝐴 , 0R ⟩ = ⟨ 𝐵 , 0R ⟩ ↔ 𝐴 = 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		eqresr.1	⊢ 𝐴 ∈ V
2		eqid	⊢ 0R = 0R
3		0r	⊢ 0R ∈ R
4	3	elexi	⊢ 0R ∈ V
5	1 4	opth	⊢ ( ⟨ 𝐴 , 0R ⟩ = ⟨ 𝐵 , 0R ⟩ ↔ ( 𝐴 = 𝐵 ∧ 0R = 0R ) )
6	2 5	mpbiran2	⊢ ( ⟨ 𝐴 , 0R ⟩ = ⟨ 𝐵 , 0R ⟩ ↔ 𝐴 = 𝐵 )