Theorem caovcomg

Description: Convert an operation commutative law to class notation. (Contributed by Mario Carneiro, 1-Jun-2013)

	Ref	Expression
Hypothesis	caovcomg.1	$$⊢\left(\phi \wedge \left(x\in S\wedge y\in S\right)\right)\to xFy=yFx$$
Assertion	caovcomg	$$⊢\left(\phi \wedge \left(A\in S\wedge B\in S\right)\right)\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	1	ralrimivva	$$⊢\phi \to \forall x\in S\forall y\in SxFy=yFx$$
3		oveq1	$$⊢x=A\to xFy=AFy$$
4		oveq2	$$⊢x=A\to yFx=yFA$$
5	3 4	eqeq12d	$$⊢x=A\to \left(xFy=yFx\leftrightarrow AFy=yFA\right)$$
6		oveq2	$$⊢y=B\to AFy=AFB$$
7		oveq1	$$⊢y=B\to yFA=BFA$$
8	6 7	eqeq12d	$$⊢y=B\to \left(AFy=yFA\leftrightarrow AFB=BFA\right)$$
9	5 8	rspc2v	$$⊢\left(A\in S\wedge B\in S\right)\to \left(\forall x\in S\forall y\in SxFy=yFx\to AFB=BFA\right)$$
10	2 9	mpan9	$$⊢\left(\phi \wedge \left(A\in S\wedge B\in S\right)\right)\to AFB=BFA$$