This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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