MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  uncom Unicode version

Theorem uncom 3332
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  |-  ( A  u.  B )  =  ( B  u.  A
)

Proof of Theorem uncom
Dummy variable  x is distinct from all other variables.
StepHypRef Expression
1 orcom 376 . . 3  |-  ( ( x  e.  A  \/  x  e.  B )  <->  ( x  e.  B  \/  x  e.  A )
)
2 elun 3329 . . 3  |-  ( x  e.  ( B  u.  A )  <->  ( x  e.  B  \/  x  e.  A ) )
31, 2bitr4i 243 . 2  |-  ( ( x  e.  A  \/  x  e.  B )  <->  x  e.  ( B  u.  A ) )
43uneqri 3330 1  |-  ( A  u.  B )  =  ( B  u.  A
)
Colors of variables: wff set class
Syntax hints:    \/ wo 357    = wceq 1632    e. wcel 1696    u. cun 3163
This theorem is referenced by:  equncom  3333  uneq2  3336  un12  3346  un23  3347  ssun2  3352  unss2  3359  ssequn2  3361  undir  3431  unineq  3432  dif32  3444  disjpss  3518  undif1  3542  undif2  3543  difcom  3551  uneqdifeq  3555  dfif4  3589  dfif5  3590  prcom  3718  tpass  3738  prprc1  3749  difsnid  3777  ssunsn2  3789  sspr  3793  sstp  3794  unidif0  4199  suc0  4482  difex2  4541  elpwun  4583  fresaunres2  5429  fresaunres1  5430  f1oprswap  5531  fvun2  5607  fvsnun2  5732  fsnunfv  5736  fnsuppeq0  5749  fveqf1o  5822  difxp2  6171  oev2  6538  oacomf1o  6579  undifixp  6868  dfdom2  6903  domunsncan  6978  domunsn  7027  limensuci  7053  phplem1  7056  phplem2  7057  enp1ilem  7108  findcard2  7114  findcard2s  7115  frfi  7118  domunfican  7145  elfiun  7199  infdifsn  7373  cantnfp1lem3  7398  cdacomen  7823  infunsdom1  7855  infunsdom  7856  infxp  7857  ackbij1lem2  7863  ackbij1lem18  7879  fin1a2lem10  8051  fin1a2lem13  8054  zornn0g  8148  alephadd  8215  fpwwe2lem13  8280  canthp1lem1  8290  xrsupss  10643  xrinfmss  10644  supxrmnf  10652  prunioo  10780  fzsuc2  10858  fseq1p1m1  10873  hashinf  11358  hashun3  11382  hashbclem  11406  incexclem  12311  ramub1lem1  13089  setsid  13203  mreexexlem3d  13564  mreexexlem4d  13565  cnvtsr  14347  dmdprdsplit2  15297  lspsnat  15914  lsppratlem3  15918  indistopon  16754  indistps  16764  indistps2  16765  ordtcnv  16947  leordtval2  16958  lecldbas  16965  cmpcld  17145  iuncon  17170  ufprim  17620  alexsubALTlem3  17759  ptcmplem1  17762  xpsdsval  17961  iccntr  18342  reconn  18349  volun  18918  voliunlem1  18923  icombl  18937  ioombl  18938  ismbf3d  19025  i1f1  19061  itgioo  19186  itgsplitioo  19208  lhop  19379  plyeq0  19609  fta1lem  19703  birthdaylem2  20263  lgsquadlem2  20610  ex-dif  20826  shjcom  21953  fmptpr  23229  difioo  23290  xrge0iifcnv  23330  prsiga  23507  measxun  23554  subfacp1lem1  23725  subfacp1lem3  23728  pconcon  23777  indispcon  23780  nofulllem2  24428  symdifcom  24434  symdifV  24440  hfun  24880  onint1  24960  fldcnv  25159  inabs2  25241  islimrs4  25685  hdrmp  25809  ralxpmap  26864  elrfi  26872  fzsplit1nn0  26936  eldioph2lem1  26942  eldioph2lem2  26943  diophin  26955  eldioph4b  26997  diophren  26999  kelac2  27266  pwssplit4  27294  enfixsn  27360  constr3pthlem1  28401  equncomVD  28960  bnj1416  29385  padd02  30623  paddcom  30624  pclfinclN  30761  djhcom  32217
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-v 2803  df-un 3170
  Copyright terms: Public domain W3C validator