Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  caovcomd GIF version

Theorem caovcomd 5682
 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
StepHypRef Expression
1 id 19 . 2 (𝜑𝜑)
2 caovcomd.2 . 2 (𝜑𝐴𝑆)
3 caovcomd.3 . 2 (𝜑𝐵𝑆)
4 caovcomg.1 . . 3 ((𝜑 ∧ (𝑥𝑆𝑦𝑆)) → (𝑥𝐹𝑦) = (𝑦𝐹𝑥))
54caovcomg 5681 . 2 ((𝜑 ∧ (𝐴𝑆𝐵𝑆)) → (𝐴𝐹𝐵) = (𝐵𝐹𝐴))
61, 2, 3, 5syl12anc 1142 1 (𝜑 → (𝐴𝐹𝐵) = (𝐵𝐹𝐴))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 101   = wceq 1257   ∈ wcel 1407  (class class class)co 5537 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-io 638  ax-5 1350  ax-7 1351  ax-gen 1352  ax-ie1 1396  ax-ie2 1397  ax-8 1409  ax-10 1410  ax-11 1411  ax-i12 1412  ax-bndl 1413  ax-4 1414  ax-17 1433  ax-i9 1437  ax-ial 1441  ax-i5r 1442  ax-ext 2036 This theorem depends on definitions:  df-bi 114  df-3an 896  df-tru 1260  df-nf 1364  df-sb 1660  df-clab 2041  df-cleq 2047  df-clel 2050  df-nfc 2181  df-ral 2326  df-rex 2327  df-v 2574  df-un 2947  df-sn 3406  df-pr 3407  df-op 3409  df-uni 3606  df-br 3790  df-iota 4892  df-fv 4935  df-ov 5540 This theorem is referenced by:  caovcanrd  5689  caovord2d  5695  caovdir2d  5702  caov32d  5706  caov12d  5707  caov31d  5708  caov411d  5711  caov42d  5712  caovimo  5719  ecopovsymg  6233  ecopoverg  6235  ltsonq  6524  prarloclemlo  6620  addextpr  6747  ltsosr  6877  ltasrg  6883  mulextsr1lem  6892
 Copyright terms: Public domain W3C validator