Theorem poeq2

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

	Ref	Expression
Assertion	poeq2	$$⊢A=B\to \left(R\mathrm{Po}A\leftrightarrow R\mathrm{Po}B\right)$$

Proof

Step	Hyp	Ref	Expression
1		eqimss2	$$⊢A=B\to B\subseteq A$$
2		poss	$$⊢B\subseteq A\to \left(R\mathrm{Po}A\to R\mathrm{Po}B\right)$$
3	1 2	syl	$$⊢A=B\to \left(R\mathrm{Po}A\to R\mathrm{Po}B\right)$$
4		eqimss	$$⊢A=B\to A\subseteq B$$
5		poss	$$⊢A\subseteq B\to \left(R\mathrm{Po}B\to R\mathrm{Po}A\right)$$
6	4 5	syl	$$⊢A=B\to \left(R\mathrm{Po}B\to R\mathrm{Po}A\right)$$
7	3 6	impbid	$$⊢A=B\to \left(R\mathrm{Po}A\leftrightarrow R\mathrm{Po}B\right)$$