Metamath Proof Explorer

Theorem caovord

Description: Convert an operation ordering law to class notation. (Contributed by NM, 19-Feb-1996)

Ref Expression
Hypotheses caovord.1 ⊢ A ∈ V
caovord.2 ⊢ B ∈ V
caovord.3 ⊢ z ∈ S → x R y ↔ z F x R z F y
Assertion caovord ⊢ C ∈ S → A R B ↔ C F A R C F B

Proof

Step Hyp Ref Expression
1 caovord.1 ⊢ A ∈ V
2 caovord.2 ⊢ B ∈ V
3 caovord.3 ⊢ z ∈ S → x R y ↔ z F x R z F y
4 oveq1 ⊢ z = C → z F A = C F A
5 oveq1 ⊢ z = C → z F B = C F B
6 4 5 breq12d ⊢ z = C → z F A R z F B ↔ C F A R C F B
7 6 bibi2d ⊢ z = C → A R B ↔ z F A R z F B ↔ A R B ↔ C F A R C F B
8 breq1 ⊢ x = A → x R y ↔ A R y
9 oveq2 ⊢ x = A → z F x = z F A
10 9 breq1d ⊢ x = A → z F x R z F y ↔ z F A R z F y
11 8 10 bibi12d ⊢ x = A → x R y ↔ z F x R z F y ↔ A R y ↔ z F A R z F y
12 breq2 ⊢ y = B → A R y ↔ A R B
13 oveq2 ⊢ y = B → z F y = z F B
14 13 breq2d ⊢ y = B → z F A R z F y ↔ z F A R z F B
15 12 14 bibi12d ⊢ y = B → A R y ↔ z F A R z F y ↔ A R B ↔ z F A R z F B
16 11 15 sylan9bb ⊢ x = A ∧ y = B → x R y ↔ z F x R z F y ↔ A R B ↔ z F A R z F B
17 16 imbi2d ⊢ x = A ∧ y = B → z ∈ S → x R y ↔ z F x R z F y ↔ z ∈ S → A R B ↔ z F A R z F B
18 1 2 17 3 vtocl2 ⊢ z ∈ S → A R B ↔ z F A R z F B
19 7 18 vtoclga ⊢ C ∈ S → A R B ↔ C F A R C F B