Theorem uncom 4160

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 884	. . 3 ⊢ ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) ↔ (𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐴))
2		elun 4155	. . 3 ⊢ (𝑥 ∈ (𝐵 ∪ 𝐴) ↔ (𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐴))
3	1, 2	bitr4i 281	. 2 ⊢ ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ (𝐵 ∪ 𝐴))
4	3	uneqri 4158	1 ⊢ (𝐴 ∪ 𝐵) = (𝐵 ∪ 𝐴)

This proof depends on syntax axioms:   ∨ wo 861   = wceq 1570   ∈ wcel 2147   ∪ cun 4152

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-un 4154

This theorem is used by:  equncom  4161  uneq2  4164  un12  4174  un23  4175  ssun2  4180  unss2  4188  ssequn2  4190  symdifcom  4202  undir  4235  unineq  4236  dif32  4250  0un  4349  disjpss  4417  undif1  4433  undif2  4434  difcom  4447  uneqdifeq  4451  dfif4  4501  dfif5  4502  pwundif  4586  prcom  4693  tpass  4713  prprc1  4726  ssunsn2  4786  sstp  4794  unidif0OLD  5327  difxp2  6170  suc0  6461  fununfunOLD  6612  fnunres2  6677  fresaunres2  6779  fresaunres1  6780  f1oprswap  6896  fvun2  7003  fvsnun2  7214  fsnunfv  7218  fveqf1o  7336  difex2  7801  elpwun  7810  fnsuppeq0  8240  oev2  8562  oacomf1o  8604  undifixp  8993  dfdom2  9036  domunsncan  9127  enfixsn  9136  domunsn  9177  limensuci  9203  findcard2  9211  findcard2s  9212  unfi  9217  ssfi  9219  enp1ilem  9300  frfi  9307  domunfican  9344  fsuppunbi  9411  elfiun  9452  infdifsn  9688  cantnfp1lem3  9711  rankmapu  9925  hfunOLD  9949  djuunxp  10032  infunsdom1  10320  infunsdom  10321  infxp  10322  ackbij1lem2  10328  ackbij1lem18  10344  fin1a2lem10  10517  fin1a2lem13  10520  zornn0g  10613  alephadd  10692  fpwwe2lem12  10757  canthp1lem1  10767  xrsupss  13469  xrinfmss  13470  supxrmnf  13477  prunioo  13642  fzsuc2  13746  fzdifsuc  13748  fseq1p1m1  13762  f1resfz0f1d  13957  hashinf  14509  hashun3  14558  hashbclem  14627  relexpcnv  15220  fsumsplit1  15943  modfsummods  15992  incexclem  16037  lcmfunsnlem  16848  ramub1lem1  17236  setsid  17417  mreexexlem3d  17852  mreexexlem4d  17853  cnvtsr  18794  symgvalstruct  19644  gsumzaddlem  20168  gsummptfzsplitl  20180  dmdprdsplit2  20295  lspsnat  21456  lsppratlem3  21460  lindsenlbs  22190  indistopon  23352  indistps  23362  indistps2  23363  ordtcnv  23552  leordtval2  23563  lecldbas  23570  cmpcld  23753  iunconn  23779  ufprim  24261  alexsubALTlem3  24401  ptcmplem1  24404  xpsdsval  24733  iccntr  25174  reconn  25181  volun  25899  voliunlem1  25904  icombl  25918  ioombl  25919  ismbf3d  26008  itgioo  26169  itgsplitioo  26191  lhop  26369  plyeq0  26563  fta1lem  26661  birthdaylem2  27313  lgsquadlem2  27741  nosepdm  28074  addscom  28385  addsproplem4  28391  addsproplem6  28393  negsproplem4  28450  negsproplem6  28452  negbdaylem  28475  mulscom  28558  mulsass  28585  usgrfilem  29941  ex-dif  31057  shjcom  31993  indifundif  33195  imadifxp  33270  difioo  33447  nn0diffz0  33459  gsummulsubdishift1  33705  symgcom  33720  pmtrcnel2  33727  cycpmcl  33753  cycpm2tr  33756  tocyccntz  33781  lindsunlem  34339  lindsun  34340  fldext2rspun  34397  ordtcnvNEW  34635  xrge0iifcnv  34648  prsiga  34846  unelldsys  34874  measun  34927  measunl  34932  difelcarsg  35025  carsgclctunlem1  35032  carsggect  35033  eulerpartgbij  35087  circlemethhgt  35355  hgt750lemb  35368  bnj1416  35752  subfacp1lem1  36124  subfacp1lem3  36127  pconnconn  36176  indispconn  36179  satfv1lem  36307  onint1  37428  bj-fununsn2  38380  pibt2  38545  poimirlem3  38746  poimirlem5  38748  poimirlem11  38754  poimirlem12  38755  poimirlem13  38756  poimirlem14  38757  poimirlem15  38758  poimirlem16  38759  poimirlem19  38762  poimirlem20  38763  poimirlem21  38764  poimirlem22  38765  poimirlem28  38771  poimirlem30  38773  ecuncnvepres  39530  padd02  41072  paddcom  41073  pclfinclN  41210  djhcom  42665  elrfi  43909  fzsplit1nn0  43969  eldioph2lem1  43975  eldioph2lem2  43976  diophin  43987  eldioph4b  44022  diophren  44024  kelac2  44271  pwssplit4  44295  iocunico  44416  rp-fakeuninass  44720  iunrelexp0  44905  corcltrcl  44942  frege124d  44964  mnuprdlem1  45459  equncomVD  46052  iunconnlem2  46119  snunioo1  46739  iccdifioo  46742  limciccioolb  46848  sumnnodd  46857  dirkercncflem2  47329  dirkercncflem3  47330  fourierdlem32  47364  fourierdlem93  47424  isomenndlem  47755  hoidmvlelem2  47821  hspmbllem1  47851  hspmbllem2  47852  fsumsplitsndif  48666  isubgr3stgrlem1  49279  usgrexmpl1edg  49337  usgrexmpl2edg  49342  aacllem  51251