This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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