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	|- ( ( ( A e. P. /\ B e. P. ) /\ ( C e. P. /\ D e. P. ) ) -> ( [ <. A , B >. ] ~R = [ <. C , D >. ] ~R <-> ( A +P. D ) = ( B +P. C ) ) )

Proof

Step	Hyp	Ref	Expression
1		enrer	|- ~R Er ( P. X. P. )
2	1	a1i	|- ( ( ( A e. P. /\ B e. P. ) /\ ( C e. P. /\ D e. P. ) ) -> ~R Er ( P. X. P. ) )
3		opelxpi	|- ( ( A e. P. /\ B e. P. ) -> <. A , B >. e. ( P. X. P. ) )
4	3	adantr	|- ( ( ( A e. P. /\ B e. P. ) /\ ( C e. P. /\ D e. P. ) ) -> <. A , B >. e. ( P. X. P. ) )
5	2 4	erth	|- ( ( ( A e. P. /\ B e. P. ) /\ ( C e. P. /\ D e. P. ) ) -> ( <. A , B >. ~R <. C , D >. <-> [ <. A , B >. ] ~R = [ <. C , D >. ] ~R ) )
6		enrbreq	|- ( ( ( A e. P. /\ B e. P. ) /\ ( C e. P. /\ D e. P. ) ) -> ( <. A , B >. ~R <. C , D >. <-> ( A +P. D ) = ( B +P. C ) ) )
7	5 6	bitr3d	|- ( ( ( A e. P. /\ B e. P. ) /\ ( C e. P. /\ D e. P. ) ) -> ( [ <. A , B >. ] ~R = [ <. C , D >. ] ~R <-> ( A +P. D ) = ( B +P. C ) ) )