Theorem soeq1

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

	Ref	Expression
Assertion	soeq1	$$⊢R=S\to \left(R\mathrm{Or}A\leftrightarrow S\mathrm{Or}A\right)$$

Proof

Step	Hyp	Ref	Expression
1		poeq1	$$⊢R=S\to \left(R\mathrm{Po}A\leftrightarrow S\mathrm{Po}A\right)$$
2		breq	$$⊢R=S\to \left(xRy\leftrightarrow xSy\right)$$
3		biidd	$$⊢R=S\to \left(x=y\leftrightarrow x=y\right)$$
4		breq	$$⊢R=S\to \left(yRx\leftrightarrow ySx\right)$$
5	2 3 4	3orbi123d	$$⊢R=S\to \left(\left(xRy\vee x=y\vee yRx\right)\leftrightarrow \left(xSy\vee x=y\vee ySx\right)\right)$$
6	5	2ralbidv	$$⊢R=S\to \left(\forall x\in A\forall y\in A\left(xRy\vee x=y\vee yRx\right)\leftrightarrow \forall x\in A\forall y\in A\left(xSy\vee x=y\vee ySx\right)\right)$$
7	1 6	anbi12d	$$⊢R=S\to \left(\left(R\mathrm{Po}A\wedge \forall x\in A\forall y\in A\left(xRy\vee x=y\vee yRx\right)\right)\leftrightarrow \left(S\mathrm{Po}A\wedge \forall x\in A\forall y\in A\left(xSy\vee x=y\vee ySx\right)\right)\right)$$
8		df-so	$$⊢R\mathrm{Or}A\leftrightarrow \left(R\mathrm{Po}A\wedge \forall x\in A\forall y\in A\left(xRy\vee x=y\vee yRx\right)\right)$$
9		df-so	$$⊢S\mathrm{Or}A\leftrightarrow \left(S\mathrm{Po}A\wedge \forall x\in A\forall y\in A\left(xSy\vee x=y\vee ySx\right)\right)$$
10	7 8 9	3bitr4g	$$⊢R=S\to \left(R\mathrm{Or}A\leftrightarrow S\mathrm{Or}A\right)$$