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

Metamath Proof Explorer

Theorem caovcan

Description: Convert an operation cancellation law to class notation. (Contributed by NM, 20-Aug-1995)

Ref Expression
Hypotheses caovcan.1 ⊢ C ∈ V
caovcan.2 ⊢ x ∈ S ∧ y ∈ S → x F y = x F z → y = z
Assertion caovcan ⊢ A ∈ S ∧ B ∈ S → A F B = A F C → B = C

Proof

Step Hyp Ref Expression
1 caovcan.1 ⊢ C ∈ V
2 caovcan.2 ⊢ x ∈ S ∧ y ∈ S → x F y = x F z → y = z
3 oveq1 ⊢ x = A → x F y = A F y
4 oveq1 ⊢ x = A → x F C = A F C
5 3 4 eqeq12d ⊢ x = A → x F y = x F C ↔ A F y = A F C
6 5 imbi1d ⊢ x = A → x F y = x F C → y = C ↔ A F y = A F C → y = C
7 oveq2 ⊢ y = B → A F y = A F B
8 7 eqeq1d ⊢ y = B → A F y = A F C ↔ A F B = A F C
9 eqeq1 ⊢ y = B → y = C ↔ B = C
10 8 9 imbi12d ⊢ y = B → A F y = A F C → y = C ↔ A F B = A F C → B = C
11 oveq2 ⊢ z = C → x F z = x F C
12 11 eqeq2d ⊢ z = C → x F y = x F z ↔ x F y = x F C
13 eqeq2 ⊢ z = C → y = z ↔ y = C
14 12 13 imbi12d ⊢ z = C → x F y = x F z → y = z ↔ x F y = x F C → y = C
15 14 imbi2d ⊢ z = C → x ∈ S ∧ y ∈ S → x F y = x F z → y = z ↔ x ∈ S ∧ y ∈ S → x F y = x F C → y = C
16 1 15 2 vtocl ⊢ x ∈ S ∧ y ∈ S → x F y = x F C → y = C
17 6 10 16 vtocl2ga ⊢ A ∈ S ∧ B ∈ S → A F B = A F C → B = C