Metamath Proof Explorer


Theorem soeq1

Description: Equality theorem for the strict ordering predicate. (Contributed by NM, 16-Mar-1997)

Ref Expression
Assertion soeq1
|- ( R = S -> ( R Or A <-> S Or A ) )

Proof

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