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

Theorem caovcomd 5599
 Description: Convert an operation commutative law to class notation. (Contributed by Mario Carneiro, 30-Dec-2014.)
Hypotheses
Ref Expression
caovcomg.1 ((φ (x 𝑆 y 𝑆)) → (x𝐹y) = (y𝐹x))
caovcomd.2 (φA 𝑆)
caovcomd.3 (φB 𝑆)
Assertion
Ref Expression
caovcomd (φ → (A𝐹B) = (B𝐹A))
Distinct variable groups:   x,y,A   x,B,y   φ,x,y   x,𝐹,y   x,𝑆,y

Proof of Theorem caovcomd
StepHypRef Expression
1 id 19 . 2 (φφ)
2 caovcomd.2 . 2 (φA 𝑆)
3 caovcomd.3 . 2 (φB 𝑆)
4 caovcomg.1 . . 3 ((φ (x 𝑆 y 𝑆)) → (x𝐹y) = (y𝐹x))
54caovcomg 5598 . 2 ((φ (A 𝑆 B 𝑆)) → (A𝐹B) = (B𝐹A))
61, 2, 3, 5syl12anc 1132 1 (φ → (A𝐹B) = (B𝐹A))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 97   = wceq 1242   ∈ wcel 1390  (class class class)co 5455 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-10 1393  ax-11 1394  ax-i12 1395  ax-bnd 1396  ax-4 1397  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019 This theorem depends on definitions:  df-bi 110  df-3an 886  df-tru 1245  df-nf 1347  df-sb 1643  df-clab 2024  df-cleq 2030  df-clel 2033  df-nfc 2164  df-ral 2305  df-rex 2306  df-v 2553  df-un 2916  df-sn 3373  df-pr 3374  df-op 3376  df-uni 3572  df-br 3756  df-iota 4810  df-fv 4853  df-ov 5458 This theorem is referenced by:  caovcanrd  5606  caovord2d  5612  caovdir2d  5619  caov32d  5623  caov12d  5624  caov31d  5625  caov411d  5628  caov42d  5629  caovimo  5636  ecopovsymg  6141  ecopoverg  6143  ltsonq  6382  prarloclemlo  6476  addextpr  6592  ltsosr  6672  ltasrg  6678  mulextsr1lem  6686
 Copyright terms: Public domain W3C validator