Theorem uncom 4098

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	⊢ (𝐴 ∪ 𝐵) = (𝐵 ∪ 𝐴)

Proof of Theorem uncom

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		orcom 871	. . 3 ⊢ ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) ↔ (𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐴))
2		elun 4093	. . 3 ⊢ (𝑥 ∈ (𝐵 ∪ 𝐴) ↔ (𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐴))
3	1, 2	bitr4i 278	. 2 ⊢ ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ (𝐵 ∪ 𝐴))
4	3	uneqri 4096	1 ⊢ (𝐴 ∪ 𝐵) = (𝐵 ∪ 𝐴)

Syntax hints:   ∨ wo 848   = wceq 1542   ∈ wcel 2114   ∪ cun 3887

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-un 3894

This theorem is referenced by:  equncom  4099  uneq2  4102  un12  4113  un23  4114  ssun2  4119  unss2  4127  ssequn2  4129  symdifcom  4194  undir  4227  unineq  4228  dif32  4242  0un  4336  disjpss  4401  undif1  4416  undif2  4417  difcom  4428  uneqdifeq  4432  dfif4  4482  dfif5  4483  pwundif  4565  prcom  4676  tpass  4696  prprc1  4709  ssunsn2  4770  sstp  4779  unidif0OLD  5302  difxp2  6130  suc0  6400  fununfun  6546  fnunres2  6611  fresaunres2  6712  fresaunres1  6713  f1oprswap  6825  fvun2  6932  fvsnun2  7138  fsnunfv  7142  fveqf1o  7257  difex2  7714  elpwun  7723  fnsuppeq0  8142  oev2  8458  oacomf1o  8500  undifixp  8882  dfdom2  8925  domunsncan  9015  enfixsn  9024  domunsn  9065  limensuci  9091  findcard2  9099  findcard2s  9100  unfi  9105  ssfi  9107  enp1ilem  9188  frfi  9195  domunfican  9232  fsuppunbi  9302  elfiun  9343  infdifsn  9578  cantnfp1lem3  9601  rankmapu  9802  djuunxp  9845  infunsdom1  10134  infunsdom  10135  infxp  10136  ackbij1lem2  10142  ackbij1lem18  10158  fin1a2lem10  10331  fin1a2lem13  10334  zornn0g  10427  alephadd  10500  fpwwe2lem12  10565  canthp1lem1  10575  xrsupss  13261  xrinfmss  13262  supxrmnf  13269  prunioo  13434  fzsuc2  13536  fzdifsuc  13538  fseq1p1m1  13552  hashinf  14297  hashun3  14346  hashbclem  14414  relexpcnv  14997  fsumsplit1  15707  modfsummods  15756  incexclem  15801  lcmfunsnlem  16610  ramub1lem1  16997  setsid  17177  mreexexlem3d  17612  mreexexlem4d  17613  cnvtsr  18554  symgvalstruct  19372  gsumzaddlem  19896  gsummptfzsplitl  19908  dmdprdsplit2  20023  lspsnat  21143  lsppratlem3  21147  indistopon  22966  indistps  22976  indistps2  22977  ordtcnv  23166  leordtval2  23177  lecldbas  23184  cmpcld  23367  iunconn  23393  ufprim  23874  alexsubALTlem3  24014  ptcmplem1  24017  xpsdsval  24346  iccntr  24787  reconn  24794  volun  25512  voliunlem1  25517  icombl  25531  ioombl  25532  ismbf3d  25621  itgioo  25783  itgsplitioo  25805  lhop  25983  plyeq0  26176  fta1lem  26273  birthdaylem2  26916  lgsquadlem2  27344  nosepdm  27648  addscom  27958  addsproplem4  27964  addsproplem6  27966  negsproplem4  28023  negsproplem6  28025  negbdaylem  28048  mulscom  28131  mulsass  28158  usgrfilem  29396  ex-dif  30493  shjcom  31429  indifundif  32594  imadifxp  32671  difioo  32855  nn0diffz0  32867  gsummulsubdishift1  33129  symgcom  33144  pmtrcnel2  33151  cycpmcl  33177  cycpm2tr  33180  tocyccntz  33205  lindsunlem  33768  lindsun  33769  fldext2rspun  33826  ordtcnvNEW  34064  xrge0iifcnv  34077  prsiga  34275  unelldsys  34302  measun  34355  measunl  34360  difelcarsg  34454  carsgclctunlem1  34461  carsggect  34462  eulerpartgbij  34516  circlemethhgt  34787  hgt750lemb  34800  bnj1416  35181  f1resfz0f1d  35296  subfacp1lem1  35361  subfacp1lem3  35364  pconnconn  35413  indispconn  35416  satfv1lem  35544  hfun  36360  onint1  36631  bj-fununsn2  37568  pibt2  37733  lindsenlbs  37936  poimirlem3  37944  poimirlem5  37946  poimirlem11  37952  poimirlem12  37953  poimirlem13  37954  poimirlem14  37955  poimirlem15  37956  poimirlem16  37957  poimirlem19  37960  poimirlem20  37961  poimirlem21  37962  poimirlem22  37963  poimirlem28  37969  poimirlem30  37971  ecuncnvepres  38716  padd02  40258  paddcom  40259  pclfinclN  40396  djhcom  41851  elrfi  43126  fzsplit1nn0  43186  eldioph2lem1  43192  eldioph2lem2  43193  diophin  43204  eldioph4b  43239  diophren  43241  kelac2  43493  pwssplit4  43517  iocunico  43639  rp-fakeuninass  43943  iunrelexp0  44129  corcltrcl  44166  frege124d  44188  mnuprdlem1  44699  equncomVD  45294  iunconnlem2  45361  snunioo1  45942  iccdifioo  45945  limciccioolb  46051  sumnnodd  46060  dirkercncflem2  46532  dirkercncflem3  46533  fourierdlem32  46567  fourierdlem93  46627  isomenndlem  46958  hoidmvlelem2  47024  hspmbllem1  47054  hspmbllem2  47055  fsumsplitsndif  47829  isubgr3stgrlem1  48442  usgrexmpl1edg  48500  usgrexmpl2edg  48505  aacllem  50276