Theorem caovcomd

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

	Ref	Expression
Hypotheses	caovcomg.1	$$⊢\left(\phi \wedge \left(x\in S\wedge y\in S\right)\right)\to xFy=yFx$$
	caovcomd.2	$$⊢\phi \to A\in S$$
	caovcomd.3	$$⊢\phi \to B\in S$$
Assertion	caovcomd	$$⊢\phi \to AFB=BFA$$

Proof

Step	Hyp	Ref	Expression
1		caovcomg.1	$$⊢\left(\phi \wedge \left(x\in S\wedge y\in S\right)\right)\to xFy=yFx$$
2		caovcomd.2	$$⊢\phi \to A\in S$$
3		caovcomd.3	$$⊢\phi \to B\in S$$
4		id	$$⊢\phi \to \phi$$
5	1	caovcomg	$$⊢\left(\phi \wedge \left(A\in S\wedge B\in S\right)\right)\to AFB=BFA$$
6	4 2 3 5	syl12anc	$$⊢\phi \to AFB=BFA$$