Metamath Proof Explorer

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 ∈ V
caovcom.2 ⊢ B ∈ V
caovcom.3 ⊢ x F y = y F x
Assertion caovcom ⊢ A F B = B F A

Proof

Step Hyp Ref Expression
1 caovcom.1 ⊢ A ∈ V
2 caovcom.2 ⊢ B ∈ V
3 caovcom.3 ⊢ x F y = y F x
4 1 2 pm3.2i ⊢ A ∈ V ∧ B ∈ V
5 3 a1i ⊢ A ∈ V ∧ x ∈ V ∧ y ∈ V → x F y = y F x
6 5 caovcomg ⊢ A ∈ V ∧ A ∈ V ∧ B ∈ V → A F B = B F A
7 1 4 6 mp2an ⊢ A F B = B F A