caovcan

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

Step	Hyp	Ref	Expression
1		caovcan.1	$⊢ C \in V$
2		caovcan.2	$⊢ (x \in S \land y \in S) \to (x F y = x F z \to y = z)$
3		oveq1	$⊢ x = A \to x F y = A F y$
4		oveq1	$⊢ x = A \to x F C = A F C$
5	3 4	eqeq12d	$⊢ x = A \to (x F y = x F C \leftrightarrow A F y = A F C)$
6	5	imbi1d	$⊢ x = A \to ((x F y = x F C \to y = C) \leftrightarrow (A F y = A F C \to y = C))$
7		oveq2	$⊢ y = B \to A F y = A F B$
8	7	eqeq1d	$⊢ y = B \to (A F y = A F C \leftrightarrow A F B = A F C)$
9		eqeq1	$⊢ y = B \to (y = C \leftrightarrow B = C)$
10	8 9	imbi12d	$⊢ y = B \to ((A F y = A F C \to y = C) \leftrightarrow (A F B = A F C \to B = C))$
11		oveq2	$⊢ z = C \to x F z = x F C$
12	11	eqeq2d	$⊢ z = C \to (x F y = x F z \leftrightarrow x F y = x F C)$
13		eqeq2	$⊢ z = C \to (y = z \leftrightarrow y = C)$
14	12 13	imbi12d	$⊢ z = C \to ((x F y = x F z \to y = z) \leftrightarrow (x F y = x F C \to y = C))$
15	14	imbi2d	$⊢ z = C \to (((x \in S \land y \in S) \to (x F y = x F z \to y = z)) \leftrightarrow ((x \in S \land y \in S) \to (x F y = x F C \to y = C)))$
16	1 15 2	vtocl	$⊢ (x \in S \land y \in S) \to (x F y = x F C \to y = C)$
17	6 10 16	vtocl2ga	$⊢ (A \in S \land B \in S) \to (A F B = A F C \to B = C)$

Metamath Proof Explorer