Theorem poeq1

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

	Ref	Expression
Assertion	poeq1	⊢ ( 𝑅 = 𝑆 → ( 𝑅 Po 𝐴 ↔ 𝑆 Po 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		breq	⊢ ( 𝑅 = 𝑆 → ( 𝑥 𝑅 𝑥 ↔ 𝑥 𝑆 𝑥 ) )
2	1	notbid	⊢ ( 𝑅 = 𝑆 → ( ¬ 𝑥 𝑅 𝑥 ↔ ¬ 𝑥 𝑆 𝑥 ) )
3		breq	⊢ ( 𝑅 = 𝑆 → ( 𝑥 𝑅 𝑦 ↔ 𝑥 𝑆 𝑦 ) )
4		breq	⊢ ( 𝑅 = 𝑆 → ( 𝑦 𝑅 𝑧 ↔ 𝑦 𝑆 𝑧 ) )
5	3 4	anbi12d	⊢ ( 𝑅 = 𝑆 → ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) ↔ ( 𝑥 𝑆 𝑦 ∧ 𝑦 𝑆 𝑧 ) ) )
6		breq	⊢ ( 𝑅 = 𝑆 → ( 𝑥 𝑅 𝑧 ↔ 𝑥 𝑆 𝑧 ) )
7	5 6	imbi12d	⊢ ( 𝑅 = 𝑆 → ( ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) ↔ ( ( 𝑥 𝑆 𝑦 ∧ 𝑦 𝑆 𝑧 ) → 𝑥 𝑆 𝑧 ) ) )
8	2 7	anbi12d	⊢ ( 𝑅 = 𝑆 → ( ( ¬ 𝑥 𝑅 𝑥 ∧ ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) ) ↔ ( ¬ 𝑥 𝑆 𝑥 ∧ ( ( 𝑥 𝑆 𝑦 ∧ 𝑦 𝑆 𝑧 ) → 𝑥 𝑆 𝑧 ) ) ) )
9	8	ralbidv	⊢ ( 𝑅 = 𝑆 → ( ∀ 𝑧 ∈ 𝐴 ( ¬ 𝑥 𝑅 𝑥 ∧ ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) ) ↔ ∀ 𝑧 ∈ 𝐴 ( ¬ 𝑥 𝑆 𝑥 ∧ ( ( 𝑥 𝑆 𝑦 ∧ 𝑦 𝑆 𝑧 ) → 𝑥 𝑆 𝑧 ) ) ) )
10	9	2ralbidv	⊢ ( 𝑅 = 𝑆 → ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐴 ( ¬ 𝑥 𝑅 𝑥 ∧ ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) ) ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐴 ( ¬ 𝑥 𝑆 𝑥 ∧ ( ( 𝑥 𝑆 𝑦 ∧ 𝑦 𝑆 𝑧 ) → 𝑥 𝑆 𝑧 ) ) ) )
11		df-po	⊢ ( 𝑅 Po 𝐴 ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐴 ( ¬ 𝑥 𝑅 𝑥 ∧ ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) ) )
12		df-po	⊢ ( 𝑆 Po 𝐴 ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐴 ( ¬ 𝑥 𝑆 𝑥 ∧ ( ( 𝑥 𝑆 𝑦 ∧ 𝑦 𝑆 𝑧 ) → 𝑥 𝑆 𝑧 ) ) )
13	10 11 12	3bitr4g	⊢ ( 𝑅 = 𝑆 → ( 𝑅 Po 𝐴 ↔ 𝑆 Po 𝐴 ) )