This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem caovordg

Description: Convert an operation ordering law to class notation. (Contributed by NM, 19-Feb-1996) (Revised by Mario Carneiro, 30-Dec-2014)

Ref Expression
Hypothesis caovordg.1 ⊢ φ ∧ x ∈ S ∧ y ∈ S ∧ z ∈ S → x R y ↔ z F x R z F y
Assertion caovordg ⊢ φ ∧ A ∈ S ∧ B ∈ S ∧ C ∈ S → A R B ↔ C F A R C F B

Proof

Step Hyp Ref Expression
1 caovordg.1 ⊢ φ ∧ x ∈ S ∧ y ∈ S ∧ z ∈ S → x R y ↔ z F x R z F y
2 1 ralrimivvva ⊢ φ → ∀ x ∈ S ∀ y ∈ S ∀ z ∈ S x R y ↔ z F x R z F y
3 breq1 ⊢ x = A → x R y ↔ A R y
4 oveq2 ⊢ x = A → z F x = z F A
5 4 breq1d ⊢ x = A → z F x R z F y ↔ z F A R z F y
6 3 5 bibi12d ⊢ x = A → x R y ↔ z F x R z F y ↔ A R y ↔ z F A R z F y
7 breq2 ⊢ y = B → A R y ↔ A R B
8 oveq2 ⊢ y = B → z F y = z F B
9 8 breq2d ⊢ y = B → z F A R z F y ↔ z F A R z F B
10 7 9 bibi12d ⊢ y = B → A R y ↔ z F A R z F y ↔ A R B ↔ z F A R z F B
11 oveq1 ⊢ z = C → z F A = C F A
12 oveq1 ⊢ z = C → z F B = C F B
13 11 12 breq12d ⊢ z = C → z F A R z F B ↔ C F A R C F B
14 13 bibi2d ⊢ z = C → A R B ↔ z F A R z F B ↔ A R B ↔ C F A R C F B
15 6 10 14 rspc3v ⊢ A ∈ S ∧ B ∈ S ∧ C ∈ S → ∀ x ∈ S ∀ y ∈ S ∀ z ∈ S x R y ↔ z F x R z F y → A R B ↔ C F A R C F B
16 2 15 mpan9 ⊢ φ ∧ A ∈ S ∧ B ∈ S ∧ C ∈ S → A R B ↔ C F A R C F B