Theorem caovcom

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

	Ref	Expression
Hypotheses	caovcom.1	$$⊢A\in \mathrm{V}$$
	caovcom.2	$$⊢B\in \mathrm{V}$$
	caovcom.3	$$⊢xFy=yFx$$
Assertion	caovcom	$$⊢AFB=BFA$$

Proof

Step	Hyp	Ref	Expression
1		caovcom.1	$$⊢A\in \mathrm{V}$$
2		caovcom.2	$$⊢B\in \mathrm{V}$$
3		caovcom.3	$$⊢xFy=yFx$$
4	1 2	pm3.2i	$$⊢\left(A\in \mathrm{V}\wedge B\in \mathrm{V}\right)$$
5	3	a1i	$$⊢\left(A\in \mathrm{V}\wedge \left(x\in \mathrm{V}\wedge y\in \mathrm{V}\right)\right)\to xFy=yFx$$
6	5	caovcomg	$$⊢\left(A\in \mathrm{V}\wedge \left(A\in \mathrm{V}\wedge B\in \mathrm{V}\right)\right)\to AFB=BFA$$
7	1 4 6	mp2an	$$⊢AFB=BFA$$