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

Metamath Proof Explorer

Theorem caovcomd

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

	Ref	Expression
Hypotheses	caovcomg.1	$⊢ (φ \land (x \in S \land y \in S)) \to x F y = y F x$
	caovcomd.2	$⊢ φ \to A \in S$
	caovcomd.3	$⊢ φ \to B \in S$
Assertion	caovcomd	$⊢ φ \to A F B = B F A$

Step	Hyp	Ref	Expression
1		caovcomg.1	$⊢ (φ \land (x \in S \land y \in S)) \to x F y = y F x$
2		caovcomd.2	$⊢ φ \to A \in S$
3		caovcomd.3	$⊢ φ \to B \in S$
4		id	$⊢ φ \to φ$
5	1	caovcomg	$⊢ (φ \land (A \in S \land B \in S)) \to A F B = B F A$
6	4 2 3 5	syl12anc	$⊢ φ \to A F B = B F A$