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

Metamath Proof Explorer

Theorem poeq1

Description: Equality theorem for partial ordering predicate. (Contributed by NM, 27-Mar-1997)

Ref Expression
Assertion poeq1 
|- ( R = S -> ( R Po A <-> S Po A ) )

Proof

Step Hyp Ref Expression
1 breq 
 |-  ( R = S -> ( x R x <-> x S x ) )
2 1 notbid 
 |-  ( R = S -> ( -. x R x <-> -. x S x ) )
3 breq 
 |-  ( R = S -> ( x R y <-> x S y ) )
4 breq 
 |-  ( R = S -> ( y R z <-> y S z ) )
5 3 4 anbi12d 
 |-  ( R = S -> ( ( x R y /\ y R z ) <-> ( x S y /\ y S z ) ) )
6 breq 
 |-  ( R = S -> ( x R z <-> x S z ) )
7 5 6 imbi12d 
 |-  ( R = S -> ( ( ( x R y /\ y R z ) -> x R z ) <-> ( ( x S y /\ y S z ) -> x S z ) ) )
8 2 7 anbi12d 
 |-  ( R = S -> ( ( -. x R x /\ ( ( x R y /\ y R z ) -> x R z ) ) <-> ( -. x S x /\ ( ( x S y /\ y S z ) -> x S z ) ) ) )
9 8 ralbidv 
 |-  ( R = S -> ( A. z e. A ( -. x R x /\ ( ( x R y /\ y R z ) -> x R z ) ) <-> A. z e. A ( -. x S x /\ ( ( x S y /\ y S z ) -> x S z ) ) ) )
10 9 2ralbidv 
 |-  ( R = S -> ( A. x e. A A. y e. A A. z e. A ( -. x R x /\ ( ( x R y /\ y R z ) -> x R z ) ) <-> A. x e. A A. y e. A A. z e. A ( -. x S x /\ ( ( x S y /\ y S z ) -> x S z ) ) ) )
11 df-po 
 |-  ( R Po A <-> A. x e. A A. y e. A A. z e. A ( -. x R x /\ ( ( x R y /\ y R z ) -> x R z ) ) )
12 df-po 
 |-  ( S Po A <-> A. x e. A A. y e. A A. z e. A ( -. x S x /\ ( ( x S y /\ y S z ) -> x S z ) ) )
13 10 11 12 3bitr4g 
 |-  ( R = S -> ( R Po A <-> S Po A ) )