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

Theorem uncom 3319
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 3316 . . 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 3317 1  |-  ( A  u.  B )  =  ( B  u.  A
)
Colors of variables: wff set class
Syntax hints:    \/ wo 357    = wceq 1623    e. wcel 1684    u. cun 3150
This theorem is referenced by:  equncom  3320  uneq2  3323  un12  3333  un23  3334  ssun2  3339  unss2  3346  ssequn2  3348  undir  3418  unineq  3419  dif32  3431  disjpss  3505  undif1  3529  undif2  3530  difcom  3538  uneqdifeq  3542  dfif4  3576  dfif5  3577  prcom  3705  tpass  3725  prprc1  3736  difsnid  3761  ssunsn2  3773  sspr  3777  sstp  3778  unidif0  4183  suc0  4466  difex2  4525  elpwun  4567  fresaunres2  5413  fresaunres1  5414  f1oprswap  5515  fvun2  5591  fvsnun2  5716  fsnunfv  5720  fnsuppeq0  5733  fveqf1o  5806  difxp2  6155  oev2  6522  oacomf1o  6563  undifixp  6852  dfdom2  6887  domunsncan  6962  domunsn  7011  limensuci  7037  phplem1  7040  phplem2  7041  enp1ilem  7092  findcard2  7098  findcard2s  7099  frfi  7102  domunfican  7129  elfiun  7183  infdifsn  7357  cantnfp1lem3  7382  cdacomen  7807  infunsdom1  7839  infunsdom  7840  infxp  7841  ackbij1lem2  7847  ackbij1lem18  7863  fin1a2lem10  8035  fin1a2lem13  8038  zornn0g  8132  alephadd  8199  fpwwe2lem13  8264  canthp1lem1  8274  xrsupss  10627  xrinfmss  10628  supxrmnf  10636  prunioo  10764  fzsuc2  10842  fseq1p1m1  10857  hashinf  11342  hashun3  11366  hashbclem  11390  incexclem  12295  ramub1lem1  13073  setsid  13187  mreexexlem3d  13548  mreexexlem4d  13549  cnvtsr  14331  dmdprdsplit2  15281  lspsnat  15898  lsppratlem3  15902  indistopon  16738  indistps  16748  indistps2  16749  ordtcnv  16931  leordtval2  16942  lecldbas  16949  cmpcld  17129  iuncon  17154  ufprim  17604  alexsubALTlem3  17743  ptcmplem1  17746  xpsdsval  17945  iccntr  18326  reconn  18333  volun  18902  voliunlem1  18907  icombl  18921  ioombl  18922  ismbf3d  19009  i1f1  19045  itgioo  19170  itgsplitioo  19192  lhop  19363  plyeq0  19593  fta1lem  19687  birthdaylem2  20247  lgsquadlem2  20594  ex-dif  20810  shjcom  21937  difprsn2  23191  fmptpr  23214  difioo  23275  xrge0iifcnv  23315  prsiga  23492  measxun  23539  subfacp1lem1  23710  subfacp1lem3  23713  pconcon  23762  indispcon  23765  nofulllem2  24357  symdifcom  24363  symdifV  24369  hfun  24808  onint1  24888  fldcnv  25056  inabs2  25138  islimrs4  25582  hdrmp  25706  ralxpmap  26761  elrfi  26769  fzsplit1nn0  26833  eldioph2lem1  26839  eldioph2lem2  26840  diophin  26852  eldioph4b  26894  diophren  26896  kelac2  27163  pwssplit4  27191  enfixsn  27257  difprsng  28069  equncomVD  28644  bnj1416  29069  padd02  30001  paddcom  30002  pclfinclN  30139  djhcom  31595
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-v 2790  df-un 3157
  Copyright terms: Public domain W3C validator