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 𝐴 ∈ 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 ( 𝐴 𝐹 𝐵 ) = ( 𝐵 𝐹 𝐴 )