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

Theorem uncom 3229
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
StepHypRef Expression
1 orcom 378 . . 3  |-  ( ( x  e.  A  \/  x  e.  B )  <->  ( x  e.  B  \/  x  e.  A )
)
2 elun 3226 . . 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 3227 1  |-  ( A  u.  B )  =  ( B  u.  A
)
Colors of variables: wff set class
Syntax hints:    \/ wo 359    = wceq 1619    e. wcel 1621    u. cun 3076
This theorem is referenced by:  equncom  3230  uneq2  3233  un12  3243  un23  3244  ssun2  3249  unss2  3256  ssequn2  3258  undir  3325  unineq  3326  dif32  3338  disjpss  3412  undif1  3435  undif2  3436  difcom  3444  uneqdifeq  3448  dfif4  3481  dfif5  3482  prcom  3609  tpass  3629  prprc1  3640  difsnid  3661  ssunsn2  3673  sspr  3677  sstp  3678  unidif0  4077  suc0  4359  difex2  4416  elpwun  4458  fresaunres2  5270  fresaunres1  5271  f1oprswap  5372  fvun2  5443  fvsnun2  5568  fsnunfv  5572  fnsuppeq0  5585  fveqf1o  5658  difxp2  6007  oev2  6408  oacomf1o  6449  undifixp  6738  dfdom2  6773  domunsncan  6847  domunsn  6896  limensuci  6922  phplem1  6925  phplem2  6926  enp1ilem  6977  findcard2  6983  findcard2s  6984  frfi  6987  domunfican  7014  elfiun  7067  infdifsn  7241  cantnfp1lem3  7266  cdacomen  7691  infunsdom1  7723  infunsdom  7724  infxp  7725  ackbij1lem2  7731  ackbij1lem18  7747  fin1a2lem10  7919  fin1a2lem13  7922  zornn0g  8016  alephadd  8079  fpwwe2lem13  8144  canthp1lem1  8154  xrsupss  10505  xrinfmss  10506  supxrmnf  10514  prunioo  10642  fzsuc2  10720  fseq1p1m1  10735  hashinf  11220  hashbclem  11267  ramub1lem1  12947  setsid  13061  cnvtsr  14166  dmdprdsplit2  15116  lspsnat  15732  lsppratlem3  15736  indistopon  16570  indistps  16580  indistps2  16581  ordtcnv  16763  leordtval2  16774  lecldbas  16781  cmpcld  16961  iuncon  16986  ufprim  17436  alexsubALTlem3  17575  ptcmplem1  17578  xpsdsval  17777  iccntr  18158  reconn  18165  volun  18734  voliunlem1  18739  icombl  18753  ioombl  18754  ismbf3d  18841  i1f1  18877  itgioo  19002  itgsplitioo  19024  lhop  19195  plyeq0  19425  fta1lem  19519  birthdaylem2  20079  lgsquadlem2  20426  ex-dif  20623  shjcom  21767  subfacp1lem1  22881  subfacp1lem3  22884  pconcon  22933  indispcon  22936  axfelem10  23523  axfelem14  23527  symdifcom  23538  symdifV  23544  hfun  23982  onint1  24062  fldcnv  24221  inabs2  24304  repfuntw  24326  islimrs4  24748  hdrmp  24872  ralxpmap  25927  elrfi  25935  fzsplit1nn0  25999  eldioph2lem1  26005  eldioph2lem2  26006  diophin  26018  eldioph4b  26060  diophren  26062  kelac2  26329  pwssplit4  26357  enfixsn  26423  equncomVD  27334  bnj1416  27758  padd02  28690  paddcom  28691  pclfinclN  28828  djhcom  30284
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1926  ax-ext 2234
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1883  df-clab 2240  df-cleq 2246  df-clel 2249  df-nfc 2374  df-v 2729  df-un 3083
  Copyright terms: Public domain W3C validator