Theorem uncom 4083

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 866	. . 3 ⊢ ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) ↔ (𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐴))
2		elun 4079	. . 3 ⊢ (𝑥 ∈ (𝐵 ∪ 𝐴) ↔ (𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐴))
3	1, 2	bitr4i 277	. 2 ⊢ ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ (𝐵 ∪ 𝐴))
4	3	uneqri 4081	1 ⊢ (𝐴 ∪ 𝐵) = (𝐵 ∪ 𝐴)

Syntax hints:   ∨ wo 843   = wceq 1539   ∈ wcel 2108   ∪ cun 3881

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-un 3888

This theorem is referenced by:  equncom  4084  uneq2  4087  un12  4097  un23  4098  ssun2  4103  unss2  4111  ssequn2  4113  symdifcom  4174  undir  4207  unineq  4208  dif32  4223  0un  4323  disjpss  4391  undif1  4406  undif2  4407  difcom  4416  uneqdifeq  4420  dfif4  4471  dfif5  4472  pwundif  4556  prcom  4665  tpass  4685  prprc1  4698  difsnid  4740  ssunsn2  4757  sspr  4763  sstp  4764  symdifv  5011  iunxdif3  5020  unidif0  5277  difxp2  6058  suc0  6325  fununfun  6466  fresaunres2  6630  fresaunres1  6631  f1oprswap  6743  fvun2  6842  fvsnun2  7037  fsnunfv  7041  fveqf1o  7155  f1ofvswap  7158  difex2  7588  elpwun  7597  fnsuppeq0  7979  oev2  8315  oacomf1o  8358  ralxpmap  8642  undifixp  8680  dfdom2  8721  domunsncan  8812  enfixsn  8821  domunsn  8863  limensuci  8889  phplem2  8893  findcard2  8909  findcard2s  8910  unfi  8917  ssfi  8918  enp1ilem  8981  findcard2OLD  8986  frfi  8989  domunfican  9017  fsuppunbi  9079  elfiun  9119  infdifsn  9345  cantnfp1lem3  9368  rankmapu  9567  djuunxp  9610  infunsdom1  9900  infunsdom  9901  infxp  9902  ackbij1lem2  9908  ackbij1lem18  9924  fin1a2lem10  10096  fin1a2lem13  10099  zornn0g  10192  alephadd  10264  fpwwe2lem12  10329  canthp1lem1  10339  xrsupss  12972  xrinfmss  12973  supxrmnf  12980  prunioo  13142  fzsuc2  13243  fzdifsuc  13245  fseq1p1m1  13259  hashinf  13977  hashun3  14027  hashbclem  14092  relexpcnv  14674  fsumsplit1  15385  modfsummods  15433  incexclem  15476  lcmfunsnlem  16274  ramub1lem1  16655  setsid  16837  mreexexlem3d  17272  mreexexlem4d  17273  cnvtsr  18221  symgvalstruct  18919  symgvalstructOLD  18920  gsumzaddlem  19437  gsummptfzsplitl  19449  dmdprdsplit2  19564  lspsnat  20322  lsppratlem3  20326  indistopon  22059  indistps  22069  indistps2  22070  ordtcnv  22260  leordtval2  22271  lecldbas  22278  cmpcld  22461  iunconn  22487  ufprim  22968  alexsubALTlem3  23108  ptcmplem1  23111  xpsdsval  23442  iccntr  23890  reconn  23897  volun  24614  voliunlem1  24619  icombl  24633  ioombl  24634  ismbf3d  24723  itgioo  24885  itgsplitioo  24907  lhop  25085  plyeq0  25277  fta1lem  25372  birthdaylem2  26007  lgsquadlem2  26434  usgrfilem  27597  ex-dif  28688  shjcom  29621  undifr  30773  indifundif  30774  imadifxp  30841  fnunres2  30917  difioo  31005  symgcom  31254  pmtrcnel2  31261  cycpmcl  31285  cycpm2tr  31288  tocyccntz  31313  lindsunlem  31607  lindsun  31608  ordtcnvNEW  31772  xrge0iifcnv  31785  prsiga  31999  unelldsys  32026  measun  32079  measunl  32084  difelcarsg  32177  carsgclctunlem1  32184  carsggect  32185  eulerpartgbij  32239  circlemethhgt  32523  hgt750lemb  32536  bnj1416  32919  f1resfz0f1d  32972  subfacp1lem1  33041  subfacp1lem3  33044  pconnconn  33093  indispconn  33096  satfv1lem  33224  nosepdm  33814  addscom  34056  hfun  34407  onint1  34565  bj-fununsn2  35352  pibt2  35515  lindsenlbs  35699  poimirlem3  35707  poimirlem5  35709  poimirlem11  35715  poimirlem12  35716  poimirlem13  35717  poimirlem14  35718  poimirlem15  35719  poimirlem16  35720  poimirlem19  35723  poimirlem20  35724  poimirlem21  35725  poimirlem22  35726  poimirlem28  35732  poimirlem30  35734  padd02  37753  paddcom  37754  pclfinclN  37891  djhcom  39346  metakunt24  40076  elrfi  40432  fzsplit1nn0  40492  eldioph2lem1  40498  eldioph2lem2  40499  diophin  40510  eldioph4b  40549  diophren  40551  kelac2  40806  pwssplit4  40830  iocunico  40958  rp-fakeuninass  41021  iunrelexp0  41199  corcltrcl  41236  frege124d  41258  mnuprdlem1  41779  equncomVD  42377  iunconnlem2  42444  snunioo1  42940  iccdifioo  42943  limciccioolb  43052  sumnnodd  43061  dirkercncflem2  43535  dirkercncflem3  43536  fourierdlem32  43570  fourierdlem93  43630  isomenndlem  43958  hoidmvlelem2  44024  hspmbllem1  44054  hspmbllem2  44055  fsumsplitsndif  44713  aacllem  46391