Theorem uncom 4118

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

Syntax hints:   ∨ wo 845   = wceq 1541   ∈ wcel 2106   ∪ cun 3911

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-v 3448  df-un 3918

This theorem is referenced by:  equncom  4119  uneq2  4122  un12  4132  un23  4133  ssun2  4138  unss2  4146  ssequn2  4148  symdifcom  4208  undir  4241  unineq  4242  dif32  4257  0un  4357  disjpss  4425  undif1  4440  undif2  4441  difcom  4451  uneqdifeq  4455  dfif4  4506  dfif5  4507  pwundif  4589  prcom  4698  tpass  4718  prprc1  4731  difsnid  4775  ssunsn2  4792  sspr  4798  sstp  4799  symdifv  5051  iunxdif3  5060  unidif0  5320  difxp2  6123  suc0  6397  fununfun  6554  fresaunres2  6719  fresaunres1  6720  f1oprswap  6833  fvun2  6938  fvsnun2  7134  fsnunfv  7138  fveqf1o  7254  f1ofvswap  7257  difex2  7699  elpwun  7708  fnsuppeq0  8128  oev2  8474  oacomf1o  8517  ralxpmap  8841  undifixp  8879  dfdom2  8925  domunsncan  9023  enfixsn  9032  domunsn  9078  limensuci  9104  findcard2  9115  findcard2s  9116  unfi  9123  ssfi  9124  phplem2OLD  9169  enp1ilem  9229  findcard2OLD  9235  frfi  9239  domunfican  9271  fsuppunbi  9335  elfiun  9375  infdifsn  9602  cantnfp1lem3  9625  rankmapu  9823  djuunxp  9866  infunsdom1  10158  infunsdom  10159  infxp  10160  ackbij1lem2  10166  ackbij1lem18  10182  fin1a2lem10  10354  fin1a2lem13  10357  zornn0g  10450  alephadd  10522  fpwwe2lem12  10587  canthp1lem1  10597  xrsupss  13238  xrinfmss  13239  supxrmnf  13246  prunioo  13408  fzsuc2  13509  fzdifsuc  13511  fseq1p1m1  13525  hashinf  14245  hashun3  14294  hashbclem  14361  relexpcnv  14932  fsumsplit1  15641  modfsummods  15689  incexclem  15732  lcmfunsnlem  16528  ramub1lem1  16909  setsid  17091  mreexexlem3d  17540  mreexexlem4d  17541  cnvtsr  18491  symgvalstruct  19192  symgvalstructOLD  19193  gsumzaddlem  19712  gsummptfzsplitl  19724  dmdprdsplit2  19839  lspsnat  20665  lsppratlem3  20669  indistopon  22388  indistps  22398  indistps2  22399  ordtcnv  22589  leordtval2  22600  lecldbas  22607  cmpcld  22790  iunconn  22816  ufprim  23297  alexsubALTlem3  23437  ptcmplem1  23440  xpsdsval  23771  iccntr  24221  reconn  24228  volun  24946  voliunlem1  24951  icombl  24965  ioombl  24966  ismbf3d  25055  itgioo  25217  itgsplitioo  25239  lhop  25417  plyeq0  25609  fta1lem  25704  birthdaylem2  26339  lgsquadlem2  26766  nosepdm  27069  addscom  27321  addsproplem4  27327  addsproplem6  27329  negsproplem4  27372  negsproplem6  27374  usgrfilem  28338  ex-dif  29430  shjcom  30363  undifr  31515  indifundif  31516  imadifxp  31586  fnunres2  31661  difioo  31753  symgcom  32004  pmtrcnel2  32011  cycpmcl  32035  cycpm2tr  32038  tocyccntz  32063  lindsunlem  32406  lindsun  32407  ordtcnvNEW  32590  xrge0iifcnv  32603  prsiga  32819  unelldsys  32846  measun  32899  measunl  32904  difelcarsg  32999  carsgclctunlem1  33006  carsggect  33007  eulerpartgbij  33061  circlemethhgt  33345  hgt750lemb  33358  bnj1416  33740  f1resfz0f1d  33793  subfacp1lem1  33860  subfacp1lem3  33863  pconnconn  33912  indispconn  33915  satfv1lem  34043  hfun  34839  onint1  34997  bj-fununsn2  35798  pibt2  35961  lindsenlbs  36146  poimirlem3  36154  poimirlem5  36156  poimirlem11  36162  poimirlem12  36163  poimirlem13  36164  poimirlem14  36165  poimirlem15  36166  poimirlem16  36167  poimirlem19  36170  poimirlem20  36171  poimirlem21  36172  poimirlem22  36173  poimirlem28  36179  poimirlem30  36181  padd02  38348  paddcom  38349  pclfinclN  38486  djhcom  39941  metakunt24  40673  elrfi  41075  fzsplit1nn0  41135  eldioph2lem1  41141  eldioph2lem2  41142  diophin  41153  eldioph4b  41192  diophren  41194  kelac2  41450  pwssplit4  41474  iocunico  41603  rp-fakeuninass  41910  iunrelexp0  42096  corcltrcl  42133  frege124d  42155  mnuprdlem1  42674  equncomVD  43272  iunconnlem2  43339  snunioo1  43870  iccdifioo  43873  limciccioolb  43982  sumnnodd  43991  dirkercncflem2  44465  dirkercncflem3  44466  fourierdlem32  44500  fourierdlem93  44560  isomenndlem  44891  hoidmvlelem2  44957  hspmbllem1  44987  hspmbllem2  44988  fsumsplitsndif  45685  aacllem  47368