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

Metamath Proof Explorer

Theorem caovcang

Description: Convert an operation cancellation law to class notation. (Contributed by NM, 20-Aug-1995) (Revised by Mario Carneiro, 30-Dec-2014)

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

Proof

Step Hyp Ref Expression
1 caovcang.1 ⊢ φ ∧ x ∈ T ∧ y ∈ S ∧ z ∈ S → x F y = x F z ↔ y = z
2 1 ralrimivvva ⊢ φ → ∀ x ∈ T ∀ y ∈ S ∀ z ∈ 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 z = A F z
5 3 4 eqeq12d ⊢ x = A → x F y = x F z ↔ A F y = A F z
6 5 bibi1d ⊢ x = A → x F y = x F z ↔ y = z ↔ A F y = A F z ↔ y = z
7 oveq2 ⊢ y = B → A F y = A F B
8 7 eqeq1d ⊢ y = B → A F y = A F z ↔ A F B = A F z
9 eqeq1 ⊢ y = B → y = z ↔ B = z
10 8 9 bibi12d ⊢ y = B → A F y = A F z ↔ y = z ↔ A F B = A F z ↔ B = z
11 oveq2 ⊢ z = C → A F z = A F C
12 11 eqeq2d ⊢ z = C → A F B = A F z ↔ A F B = A F C
13 eqeq2 ⊢ z = C → B = z ↔ B = C
14 12 13 bibi12d ⊢ z = C → A F B = A F z ↔ B = z ↔ A F B = A F C ↔ B = C
15 6 10 14 rspc3v ⊢ A ∈ T ∧ B ∈ S ∧ C ∈ S → ∀ x ∈ T ∀ y ∈ S ∀ z ∈ S x F y = x F z ↔ y = z → A F B = A F C ↔ B = C
16 2 15 mpan9 ⊢ φ ∧ A ∈ T ∧ B ∈ S ∧ C ∈ S → A F B = A F C ↔ B = C