Theorem enreceq

Description: Equivalence class equality of positive fractions in terms of positive integers. (Contributed by NM, 29-Nov-1995) (New usage is discouraged.)

	Ref	Expression
Assertion	enreceq	⊢ ( ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) ∧ ( 𝐶 ∈ P ∧ 𝐷 ∈ P ) ) → ( [ ⟨ 𝐴 , 𝐵 ⟩ ] ~R = [ ⟨ 𝐶 , 𝐷 ⟩ ] ~R ↔ ( 𝐴 +P 𝐷 ) = ( 𝐵 +P 𝐶 ) ) )

Proof

Step	Hyp	Ref	Expression
1		enrer	⊢ ~R Er ( P × P )
2	1	a1i	⊢ ( ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) ∧ ( 𝐶 ∈ P ∧ 𝐷 ∈ P ) ) → ~R Er ( P × P ) )
3		opelxpi	⊢ ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) → ⟨ 𝐴 , 𝐵 ⟩ ∈ ( P × P ) )
4	3	adantr	⊢ ( ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) ∧ ( 𝐶 ∈ P ∧ 𝐷 ∈ P ) ) → ⟨ 𝐴 , 𝐵 ⟩ ∈ ( P × P ) )
5	2 4	erth	⊢ ( ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) ∧ ( 𝐶 ∈ P ∧ 𝐷 ∈ P ) ) → ( ⟨ 𝐴 , 𝐵 ⟩ ~R ⟨ 𝐶 , 𝐷 ⟩ ↔ [ ⟨ 𝐴 , 𝐵 ⟩ ] ~R = [ ⟨ 𝐶 , 𝐷 ⟩ ] ~R ) )
6		enrbreq	⊢ ( ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) ∧ ( 𝐶 ∈ P ∧ 𝐷 ∈ P ) ) → ( ⟨ 𝐴 , 𝐵 ⟩ ~R ⟨ 𝐶 , 𝐷 ⟩ ↔ ( 𝐴 +P 𝐷 ) = ( 𝐵 +P 𝐶 ) ) )
7	5 6	bitr3d	⊢ ( ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) ∧ ( 𝐶 ∈ P ∧ 𝐷 ∈ P ) ) → ( [ ⟨ 𝐴 , 𝐵 ⟩ ] ~R = [ ⟨ 𝐶 , 𝐷 ⟩ ] ~R ↔ ( 𝐴 +P 𝐷 ) = ( 𝐵 +P 𝐶 ) ) )