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

Theorem uncom 2972
Description: Commutative law for union of classes. Exercise 6 of [TakeutiZaring] p. 17. (Contributed by NM, 25-Jun-1998.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
Assertion
Ref Expression
uncom (AB) = (BA)

Proof of Theorem uncom
Dummy variable x is distinct from all other variables.
StepHypRef Expression
1 orcom 628 . . 3 ((x A x B) ↔ (x B x A))
2 elun 2969 . . 3 (x (BA) ↔ (x B x A))
31, 2bitr4i 174 . 2 ((x A x B) ↔ x (BA))
43uneqri 2970 1 (AB) = (BA)
Colors of variables: wff set class
Syntax hints:   wo 611   = wceq 1340   wcel 1342  cun 2800
This theorem is referenced by:  equncom  2973  uneq2  2976  un12  2986  un23  2987  ssun2  2992  unss2  2999  ssequn2  3001  undir  3072  dif32  3085  disjpss  3159  undif2ss  3180  uneqdifeqim  3189
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 97  ax-ia2 98  ax-ia3 99  ax-io 612  ax-5 1282  ax-7 1283  ax-gen 1284  ax-ie1 1329  ax-ie2 1330  ax-8 1344  ax-10 1345  ax-11 1346  ax-i12 1347  ax-bnd 1348  ax-4 1349  ax-17 1367  ax-i9 1371  ax-ial 1376  ax-i5r 1377  ax-ext 1928
This theorem depends on definitions:  df-bi 108  df-tru 1204  df-nf 1296  df-sb 1586  df-clab 1932  df-cleq 1938  df-clel 1941  df-nfc 2070  df-v 2443  df-un 2807
  Copyright terms: Public domain W3C validator