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

Theorem uncom 3065
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 634 . . 3 ((x A x B) ↔ (x B x A))
2 elun 3062 . . 3 (x (BA) ↔ (x B x A))
31, 2bitr4i 176 . 2 ((x A x B) ↔ x (BA))
43uneqri 3063 1 (AB) = (BA)
Colors of variables: wff set class
Syntax hints:   wo 616   = wceq 1373   wcel 1375  cun 2893
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 617  ax-5 1315  ax-7 1316  ax-gen 1317  ax-ie1 1362  ax-ie2 1363  ax-8 1377  ax-10 1378  ax-11 1379  ax-i12 1380  ax-bnd 1381  ax-4 1382  ax-17 1401  ax-i9 1405  ax-ial 1410  ax-i5r 1411  ax-ext 2004
This theorem depends on definitions:  df-bi 110  df-tru 1231  df-nf 1329  df-sb 1628  df-clab 2009  df-cleq 2015  df-clel 2018  df-nfc 2149  df-v 2535  df-un 2900
This theorem is referenced by:  equncom  3066  uneq2  3069  un12  3079  un23  3080  ssun2  3085  unss2  3092  ssequn2  3094  undir  3165  dif32  3178  disjpss  3256  undif2ss  3277  uneqdifeqim  3286  prcom  3397  tpass  3417  prprc1  3429  difsnss  3461  suc0  4071  fvun2  5132  fmptpr  5247  fvsnun2  5253  fsnunfv  5255
  Copyright terms: Public domain W3C validator