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 ) ) ) |