Step |
Hyp |
Ref |
Expression |
1 |
|
poeq1 |
|- ( R = S -> ( R Po A <-> S Po A ) ) |
2 |
|
breq |
|- ( R = S -> ( x R y <-> x S y ) ) |
3 |
|
biidd |
|- ( R = S -> ( x = y <-> x = y ) ) |
4 |
|
breq |
|- ( R = S -> ( y R x <-> y S x ) ) |
5 |
2 3 4
|
3orbi123d |
|- ( R = S -> ( ( x R y \/ x = y \/ y R x ) <-> ( x S y \/ x = y \/ y S x ) ) ) |
6 |
5
|
2ralbidv |
|- ( R = S -> ( A. x e. A A. y e. A ( x R y \/ x = y \/ y R x ) <-> A. x e. A A. y e. A ( x S y \/ x = y \/ y S x ) ) ) |
7 |
1 6
|
anbi12d |
|- ( R = S -> ( ( R Po A /\ A. x e. A A. y e. A ( x R y \/ x = y \/ y R x ) ) <-> ( S Po A /\ A. x e. A A. y e. A ( x S y \/ x = y \/ y S x ) ) ) ) |
8 |
|
df-so |
|- ( R Or A <-> ( R Po A /\ A. x e. A A. y e. A ( x R y \/ x = y \/ y R x ) ) ) |
9 |
|
df-so |
|- ( S Or A <-> ( S Po A /\ A. x e. A A. y e. A ( x S y \/ x = y \/ y S x ) ) ) |
10 |
7 8 9
|
3bitr4g |
|- ( R = S -> ( R Or A <-> S Or A ) ) |