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	⊢ 𝐴 ∈ V
	caovcom.2	⊢ 𝐵 ∈ V
	caovcom.3	⊢ ( 𝑥 𝐹 𝑦 ) = ( 𝑦 𝐹 𝑥 )
Assertion	caovcom	⊢ ( 𝐴 𝐹 𝐵 ) = ( 𝐵 𝐹 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		caovcom.1	⊢ 𝐴 ∈ V
2		caovcom.2	⊢ 𝐵 ∈ V
3		caovcom.3	⊢ ( 𝑥 𝐹 𝑦 ) = ( 𝑦 𝐹 𝑥 )
4	1 2	pm3.2i	⊢ ( 𝐴 ∈ V ∧ 𝐵 ∈ V )
5	3	a1i	⊢ ( ( 𝐴 ∈ V ∧ ( 𝑥 ∈ V ∧ 𝑦 ∈ V ) ) → ( 𝑥 𝐹 𝑦 ) = ( 𝑦 𝐹 𝑥 ) )
6	5	caovcomg	⊢ ( ( 𝐴 ∈ V ∧ ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ) → ( 𝐴 𝐹 𝐵 ) = ( 𝐵 𝐹 𝐴 ) )
7	1 4 6	mp2an	⊢ ( 𝐴 𝐹 𝐵 ) = ( 𝐵 𝐹 𝐴 )