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

Theorem uncom 3280
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 3277 . . 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 3278 1  |-  ( A  u.  B )  =  ( B  u.  A
)
Colors of variables: wff set class
Syntax hints:    \/ wo 359    = wceq 1619    e. wcel 1621    u. cun 3111
This theorem is referenced by:  equncom  3281  uneq2  3284  un12  3294  un23  3295  ssun2  3300  unss2  3307  ssequn2  3309  undir  3379  unineq  3380  dif32  3392  disjpss  3466  undif1  3490  undif2  3491  difcom  3499  uneqdifeq  3503  dfif4  3536  dfif5  3537  prcom  3665  tpass  3685  prprc1  3696  difsnid  3721  ssunsn2  3733  sspr  3737  sstp  3738  unidif0  4141  suc0  4424  difex2  4483  elpwun  4525  fresaunres2  5337  fresaunres1  5338  f1oprswap  5439  fvun2  5511  fvsnun2  5636  fsnunfv  5640  fnsuppeq0  5653  fveqf1o  5726  difxp2  6075  oev2  6476  oacomf1o  6517  undifixp  6806  dfdom2  6841  domunsncan  6916  domunsn  6965  limensuci  6991  phplem1  6994  phplem2  6995  enp1ilem  7046  findcard2  7052  findcard2s  7053  frfi  7056  domunfican  7083  elfiun  7137  infdifsn  7311  cantnfp1lem3  7336  cdacomen  7761  infunsdom1  7793  infunsdom  7794  infxp  7795  ackbij1lem2  7801  ackbij1lem18  7817  fin1a2lem10  7989  fin1a2lem13  7992  zornn0g  8086  alephadd  8153  fpwwe2lem13  8218  canthp1lem1  8228  xrsupss  10579  xrinfmss  10580  supxrmnf  10588  prunioo  10716  fzsuc2  10794  fseq1p1m1  10809  hashinf  11294  hashbclem  11341  ramub1lem1  13021  setsid  13135  mreexexlem3d  13496  mreexexlem4d  13497  cnvtsr  14279  dmdprdsplit2  15229  lspsnat  15846  lsppratlem3  15850  indistopon  16686  indistps  16696  indistps2  16697  ordtcnv  16879  leordtval2  16890  lecldbas  16897  cmpcld  17077  iuncon  17102  ufprim  17552  alexsubALTlem3  17691  ptcmplem1  17694  xpsdsval  17893  iccntr  18274  reconn  18281  volun  18850  voliunlem1  18855  icombl  18869  ioombl  18870  ismbf3d  18957  i1f1  18993  itgioo  19118  itgsplitioo  19140  lhop  19311  plyeq0  19541  fta1lem  19635  birthdaylem2  20195  lgsquadlem2  20542  ex-dif  20739  shjcom  21883  subfacp1lem1  23068  subfacp1lem3  23071  pconcon  23120  indispcon  23123  axfelem10  23710  axfelem14  23714  symdifcom  23725  symdifV  23731  hfun  24169  onint1  24249  fldcnv  24408  inabs2  24491  repfuntw  24513  islimrs4  24935  hdrmp  25059  ralxpmap  26114  elrfi  26122  fzsplit1nn0  26186  eldioph2lem1  26192  eldioph2lem2  26193  diophin  26205  eldioph4b  26247  diophren  26249  kelac2  26516  pwssplit4  26544  enfixsn  26610  equncomVD  27678  bnj1416  28102  padd02  29152  paddcom  29153  pclfinclN  29290  djhcom  30746
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 1927  ax-ext 2237
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 1884  df-clab 2243  df-cleq 2249  df-clel 2252  df-nfc 2381  df-v 2759  df-un 3118
  Copyright terms: Public domain W3C validator