Theorem caovcomd 6006

Description: Convert an operation commutative law to class notation. (Contributed by Mario Carneiro, 30-Dec-2014.)

Hypotheses

Ref	Expression
caovcomg.1	⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥𝐹𝑦) = (𝑦𝐹𝑥))
caovcomd.2	⊢ (𝜑 → 𝐴 ∈ 𝑆)
caovcomd.3	⊢ (𝜑 → 𝐵 ∈ 𝑆)

Assertion

Ref	Expression
caovcomd	⊢ (𝜑 → (𝐴𝐹𝐵) = (𝐵𝐹𝐴))

Distinct variable groups:   𝑥,𝑦,𝐴   𝑥,𝐵,𝑦   𝜑,𝑥,𝑦   𝑥,𝐹,𝑦   𝑥,𝑆,𝑦

Proof of Theorem caovcomd

Step	Hyp	Ref	Expression
1		id 19	. 2 ⊢ (𝜑 → 𝜑)
2		caovcomd.2	. 2 ⊢ (𝜑 → 𝐴 ∈ 𝑆)
3		caovcomd.3	. 2 ⊢ (𝜑 → 𝐵 ∈ 𝑆)
4		caovcomg.1	. . 3 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥𝐹𝑦) = (𝑦𝐹𝑥))
5	4	caovcomg 6005	. 2 ⊢ ((𝜑 ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆)) → (𝐴𝐹𝐵) = (𝐵𝐹𝐴))
6	1, 2, 3, 5	syl12anc 1231	1 ⊢ (𝜑 → (𝐴𝐹𝐵) = (𝐵𝐹𝐴))

Syntax hints:   → wi 4   ∧ wa 103   = wceq 1348   ∈ wcel 2141  (class class class)co 5850

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-3an 975  df-tru 1351  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-ral 2453  df-rex 2454  df-v 2732  df-un 3125  df-sn 3587  df-pr 3588  df-op 3590  df-uni 3795  df-br 3988  df-iota 5158  df-fv 5204  df-ov 5853

This theorem is referenced by:  caovcanrd  6013  caovord2d  6019  caovdir2d  6026  caov32d  6030  caov12d  6031  caov31d  6032  caov411d  6035  caov42d  6036  caovimo  6043  ecopovsymg  6608  ecopoverg  6610  ltsonq  7347  prarloclemlo  7443  addextpr  7570  ltsosr  7713  ltasrg  7719  mulextsr1lem  7729  seq3f1olemqsumkj  10441