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

Theorem uncom 3320
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
)
Dummy variable  x is distinct from all other variables.

Proof of Theorem uncom
StepHypRef Expression
1 orcom 378 . . 3  |-  ( ( x  e.  A  \/  x  e.  B )  <->  ( x  e.  B  \/  x  e.  A )
)
2 elun 3317 . . 3  |-  ( x  e.  ( B  u.  A )  <->  ( x  e.  B  \/  x  e.  A ) )
31, 2bitr4i 245 . 2  |-  ( ( x  e.  A  \/  x  e.  B )  <->  x  e.  ( B  u.  A ) )
43uneqri 3318 1  |-  ( A  u.  B )  =  ( B  u.  A
)
Colors of variables: wff set class
Syntax hints:    \/ wo 359    = wceq 1624    e. wcel 1685    u. cun 3151
This theorem is referenced by:  equncom  3321  uneq2  3324  un12  3334  un23  3335  ssun2  3340  unss2  3347  ssequn2  3349  undir  3419  unineq  3420  dif32  3432  disjpss  3506  undif1  3530  undif2  3531  difcom  3539  uneqdifeq  3543  dfif4  3577  dfif5  3578  prcom  3706  tpass  3726  prprc1  3737  difsnid  3762  ssunsn2  3774  sspr  3778  sstp  3779  unidif0  4182  suc0  4465  difex2  4524  elpwun  4566  fresaunres2  5378  fresaunres1  5379  f1oprswap  5480  fvun2  5552  fvsnun2  5677  fsnunfv  5681  fnsuppeq0  5694  fveqf1o  5767  difxp2  6116  oev2  6517  oacomf1o  6558  undifixp  6847  dfdom2  6882  domunsncan  6957  domunsn  7006  limensuci  7032  phplem1  7035  phplem2  7036  enp1ilem  7087  findcard2  7093  findcard2s  7094  frfi  7097  domunfican  7124  elfiun  7178  infdifsn  7352  cantnfp1lem3  7377  cdacomen  7802  infunsdom1  7834  infunsdom  7835  infxp  7836  ackbij1lem2  7842  ackbij1lem18  7858  fin1a2lem10  8030  fin1a2lem13  8033  zornn0g  8127  alephadd  8194  fpwwe2lem13  8259  canthp1lem1  8269  xrsupss  10621  xrinfmss  10622  supxrmnf  10630  prunioo  10758  fzsuc2  10836  fseq1p1m1  10851  hashinf  11336  hashun3  11360  hashbclem  11384  incexclem  12289  ramub1lem1  13067  setsid  13181  mreexexlem3d  13542  mreexexlem4d  13543  cnvtsr  14325  dmdprdsplit2  15275  lspsnat  15892  lsppratlem3  15896  indistopon  16732  indistps  16742  indistps2  16743  ordtcnv  16925  leordtval2  16936  lecldbas  16943  cmpcld  17123  iuncon  17148  ufprim  17598  alexsubALTlem3  17737  ptcmplem1  17740  xpsdsval  17939  iccntr  18320  reconn  18327  volun  18896  voliunlem1  18901  icombl  18915  ioombl  18916  ismbf3d  19003  i1f1  19039  itgioo  19164  itgsplitioo  19186  lhop  19357  plyeq0  19587  fta1lem  19681  birthdaylem2  20241  lgsquadlem2  20588  ex-dif  20785  shjcom  21929  subfacp1lem1  23114  subfacp1lem3  23117  pconcon  23166  indispcon  23169  axfelem10  23756  axfelem14  23760  symdifcom  23771  symdifV  23777  hfun  24215  onint1  24295  fldcnv  24454  inabs2  24537  repfuntw  24559  islimrs4  24981  hdrmp  25105  ralxpmap  26160  elrfi  26168  fzsplit1nn0  26232  eldioph2lem1  26238  eldioph2lem2  26239  diophin  26251  eldioph4b  26293  diophren  26295  kelac2  26562  pwssplit4  26590  enfixsn  26656  equncomVD  27912  bnj1416  28336  padd02  29268  paddcom  29269  pclfinclN  29406  djhcom  30862
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1534  ax-5 1545  ax-17 1604  ax-9 1637  ax-8 1645  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1867  ax-ext 2265
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1312  df-ex 1530  df-nf 1533  df-sb 1632  df-clab 2271  df-cleq 2277  df-clel 2280  df-nfc 2409  df-v 2791  df-un 3158
  Copyright terms: Public domain W3C validator