Metamath Proof Explorer

Theorem caovcand

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

	Ref	Expression
Hypotheses	caovcang.1	$⊢ (φ \land (x \in T \land y \in S \land z \in S)) \to (x F y = x F z \leftrightarrow y = z)$
	caovcand.2	$⊢ φ \to A \in T$
	caovcand.3	$⊢ φ \to B \in S$
	caovcand.4	$⊢ φ \to C \in S$
Assertion	caovcand	$⊢ φ \to (A F B = A F C \leftrightarrow B = C)$

Step	Hyp	Ref	Expression
1		caovcang.1	$⊢ (φ \land (x \in T \land y \in S \land z \in S)) \to (x F y = x F z \leftrightarrow y = z)$
2		caovcand.2	$⊢ φ \to A \in T$
3		caovcand.3	$⊢ φ \to B \in S$
4		caovcand.4	$⊢ φ \to C \in S$
5		id	$⊢ φ \to φ$
6	1	caovcang	$⊢ (φ \land (A \in T \land B \in S \land C \in S)) \to (A F B = A F C \leftrightarrow B = C)$
7	5 2 3 4 6	syl13anc	$⊢ φ \to (A F B = A F C \leftrightarrow B = C)$