Metamath Proof Explorer


Theorem poeq2

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

Ref Expression
Assertion poeq2
|- ( A = B -> ( R Po A <-> R Po B ) )

Proof

Step Hyp Ref Expression
1 eqimss2
 |-  ( A = B -> B C_ A )
2 poss
 |-  ( B C_ A -> ( R Po A -> R Po B ) )
3 1 2 syl
 |-  ( A = B -> ( R Po A -> R Po B ) )
4 eqimss
 |-  ( A = B -> A C_ B )
5 poss
 |-  ( A C_ B -> ( R Po B -> R Po A ) )
6 4 5 syl
 |-  ( A = B -> ( R Po B -> R Po A ) )
7 3 6 impbid
 |-  ( A = B -> ( R Po A <-> R Po B ) )