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

Theorem uncom 3063
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 3060 . . 3 (x (BA) ↔ (x B x A))
31, 2bitr4i 176 . 2 ((x A x B) ↔ x (BA))
43uneqri 3061 1 (AB) = (BA)
Colors of variables: wff set class
Syntax hints:   wo 616   = wceq 1228   wcel 1375  cun 2891
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 1316  ax-7 1317  ax-gen 1318  ax-ie1 1364  ax-ie2 1365  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 2005
This theorem depends on definitions:  df-bi 110  df-tru 1231  df-nf 1330  df-sb 1629  df-clab 2010  df-cleq 2016  df-clel 2019  df-nfc 2150  df-v 2536  df-un 2898
This theorem is referenced by:  equncom  3064  uneq2  3067  un12  3077  un23  3078  ssun2  3083  unss2  3090  ssequn2  3092  undir  3163  dif32  3176  disjpss  3254  undif2ss  3275  uneqdifeqim  3284  prcom  3419  tpass  3439  prprc1  3451  difsnss  3483  suc0  4095  fvun2  5163  fmptpr  5278  fvsnun2  5284  fsnunfv  5286  omv2  5955
  Copyright terms: Public domain W3C validator