Metamath Proof Explorer

Theorem poeq1

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

Ref Expression
Assertion poeq1 ⊢ R = S → R Po A ↔ S Po A

Proof

Step Hyp Ref Expression
1 breq ⊢ R = S → x R x ↔ x S x
2 1 notbid ⊢ R = S → ¬ x R x ↔ ¬ x S x
3 breq ⊢ R = S → x R y ↔ x S y
4 breq ⊢ R = S → y R z ↔ y S z
5 3 4 anbi12d ⊢ R = S → x R y ∧ y R z ↔ x S y ∧ y S z
6 breq ⊢ R = S → x R z ↔ x S z
7 5 6 imbi12d ⊢ R = S → x R y ∧ y R z → x R z ↔ x S y ∧ y S z → x S z
8 2 7 anbi12d ⊢ R = S → ¬ x R x ∧ x R y ∧ y R z → x R z ↔ ¬ x S x ∧ x S y ∧ y S z → x S z
9 8 ralbidv ⊢ R = S → ∀ z ∈ A ¬ x R x ∧ x R y ∧ y R z → x R z ↔ ∀ z ∈ A ¬ x S x ∧ x S y ∧ y S z → x S z
10 9 2ralbidv ⊢ R = S → ∀ x ∈ A ∀ y ∈ A ∀ z ∈ A ¬ x R x ∧ x R y ∧ y R z → x R z ↔ ∀ x ∈ A ∀ y ∈ A ∀ z ∈ A ¬ x S x ∧ x S y ∧ y S z → x S z
11 df-po ⊢ R Po A ↔ ∀ x ∈ A ∀ y ∈ A ∀ z ∈ A ¬ x R x ∧ x R y ∧ y R z → x R z
12 df-po ⊢ S Po A ↔ ∀ x ∈ A ∀ y ∈ A ∀ z ∈ A ¬ x S x ∧ x S y ∧ y S z → x S z
13 10 11 12 3bitr4g ⊢ R = S → R Po A ↔ S Po A