poeq1

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

		Ref	Expression
	Assertion	poeq1	$⊢ R = S \to (R Po A \leftrightarrow S Po A)$

Step	Hyp	Ref	Expression
1		breq	$⊢ R = S \to (x R x \leftrightarrow x S x)$
2	1	notbid	$⊢ R = S \to (\neg x R x \leftrightarrow \neg x S x)$
3		breq	$⊢ R = S \to (x R y \leftrightarrow x S y)$
4		breq	$⊢ R = S \to (y R z \leftrightarrow y S z)$
5	3 4	anbi12d	$⊢ R = S \to ((x R y \land y R z) \leftrightarrow (x S y \land y S z))$
6		breq	$⊢ R = S \to (x R z \leftrightarrow x S z)$
7	5 6	imbi12d	$⊢ R = S \to (((x R y \land y R z) \to x R z) \leftrightarrow ((x S y \land y S z) \to x S z))$
8	2 7	anbi12d	$⊢ R = S \to ((\neg x R x \land ((x R y \land y R z) \to x R z)) \leftrightarrow (\neg x S x \land ((x S y \land y S z) \to x S z)))$
9	8	ralbidv	$⊢ R = S \to (\forall z \in A (\neg x R x \land ((x R y \land y R z) \to x R z)) \leftrightarrow \forall z \in A (\neg x S x \land ((x S y \land y S z) \to x S z)))$
10	9	2ralbidv	$⊢ R = S \to (\forall x \in A \forall y \in A \forall z \in A (\neg x R x \land ((x R y \land y R z) \to x R z)) \leftrightarrow \forall x \in A \forall y \in A \forall z \in A (\neg x S x \land ((x S y \land y S z) \to x S z)))$
11		df-po	$⊢ R Po A \leftrightarrow \forall x \in A \forall y \in A \forall z \in A (\neg x R x \land ((x R y \land y R z) \to x R z))$
12		df-po	$⊢ S Po A \leftrightarrow \forall x \in A \forall y \in A \forall z \in A (\neg x S x \land ((x S y \land y S z) \to x S z))$
13	10 11 12	3bitr4g	$⊢ R = S \to (R Po A \leftrightarrow S Po A)$

Metamath Proof Explorer