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→xRy↔zFxRzFy
Assertion caovord ⊢C∈S→ARB↔CFARCFB

Proof

Step Hyp Ref Expression
1 caovord.1 ⊢A∈V
2 caovord.2 ⊢B∈V
3 caovord.3 ⊢z∈S→xRy↔zFxRzFy
4 oveq1 ⊢z=C→zFA=CFA
5 oveq1 ⊢z=C→zFB=CFB
6 4 5 breq12d ⊢z=C→zFARzFB↔CFARCFB
7 6 bibi2d ⊢z=C→ARB↔zFARzFB↔ARB↔CFARCFB
8 breq1 ⊢x=A→xRy↔ARy
9 oveq2 ⊢x=A→zFx=zFA
10 9 breq1d ⊢x=A→zFxRzFy↔zFARzFy
11 8 10 bibi12d ⊢x=A→xRy↔zFxRzFy↔ARy↔zFARzFy
12 breq2 ⊢y=B→ARy↔ARB
13 oveq2 ⊢y=B→zFy=zFB
14 13 breq2d ⊢y=B→zFARzFy↔zFARzFB
15 12 14 bibi12d ⊢y=B→ARy↔zFARzFy↔ARB↔zFARzFB
16 11 15 sylan9bb ⊢x=A∧y=B→xRy↔zFxRzFy↔ARB↔zFARzFB
17 16 imbi2d ⊢x=A∧y=B→z∈S→xRy↔zFxRzFy↔z∈S→ARB↔zFARzFB
18 1 2 17 3 vtocl2 ⊢z∈S→ARB↔zFARzFB
19 7 18 vtoclga ⊢C∈S→ARB↔CFARCFB