Theorem uncom 4111

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 881	. . 3 ⊢ ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) ↔ (𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐴))
2		elun 4106	. . 3 ⊢ (𝑥 ∈ (𝐵 ∪ 𝐴) ↔ (𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐴))
3	1, 2	bitr4i 280	. 2 ⊢ ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ (𝐵 ∪ 𝐴))
4	3	uneqri 4109	1 ⊢ (𝐴 ∪ 𝐵) = (𝐵 ∪ 𝐴)

Syntax hints:   ∨ wo 858   = wceq 1559   ∈ wcel 2141   ∪ cun 3902

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-tru 1562  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3455  df-un 3909

This theorem is referenced by:  equncom  4112  uneq2  4115  un12  4125  un23  4126  ssun2  4131  unss2  4139  ssequn2  4141  symdifcom  4206  undir  4239  unineq  4240  dif32  4254  0un  4349  disjpss  4414  undif1  4429  undif2  4430  difcom  4441  uneqdifeq  4445  dfif4  4495  dfif5  4496  pwundif  4579  prcom  4690  tpass  4710  prprc1  4723  ssunsn2  4784  sstp  4793  unidif0OLD  5316  difxp2  6148  suc0  6419  fununfun  6565  fnunres2  6630  fresaunres2  6732  fresaunres1  6733  f1oprswap  6848  fvun2  6955  fvsnun2  7163  fsnunfv  7167  fveqf1o  7282  difex2  7739  elpwun  7748  fnsuppeq0  8167  oev2  8487  oacomf1o  8529  undifixp  8912  dfdom2  8955  domunsncan  9045  enfixsn  9054  domunsn  9095  limensuci  9121  findcard2  9129  findcard2s  9130  unfi  9135  ssfi  9137  enp1ilem  9218  frfi  9225  domunfican  9262  fsuppunbi  9332  elfiun  9373  infdifsn  9609  cantnfp1lem3  9632  rankmapu  9833  djuunxp  9876  infunsdom1  10165  infunsdom  10166  infxp  10167  ackbij1lem2  10173  ackbij1lem18  10189  fin1a2lem10  10363  fin1a2lem13  10366  zornn0g  10459  alephadd  10532  fpwwe2lem12  10597  canthp1lem1  10607  xrsupss  13309  xrinfmss  13310  supxrmnf  13317  prunioo  13482  fzsuc2  13584  fzdifsuc  13586  fseq1p1m1  13600  hashinf  14345  hashun3  14394  hashbclem  14462  relexpcnv  15045  fsumsplit1  15755  modfsummods  15804  incexclem  15849  lcmfunsnlem  16658  ramub1lem1  17045  setsid  17226  mreexexlem3d  17661  mreexexlem4d  17662  cnvtsr  18603  symgvalstruct  19420  gsumzaddlem  19944  gsummptfzsplitl  19956  dmdprdsplit2  20071  lspsnat  21195  lsppratlem3  21199  indistopon  23041  indistps  23051  indistps2  23052  ordtcnv  23241  leordtval2  23252  lecldbas  23259  cmpcld  23442  iunconn  23468  ufprim  23949  alexsubALTlem3  24089  ptcmplem1  24092  xpsdsval  24421  iccntr  24862  reconn  24869  volun  25587  voliunlem1  25592  icombl  25606  ioombl  25607  ismbf3d  25696  itgioo  25858  itgsplitioo  25880  lhop  26058  plyeq0  26251  fta1lem  26348  birthdaylem2  26994  lgsquadlem2  27422  nosepdm  27725  addscom  28036  addsproplem4  28042  addsproplem6  28044  negsproplem4  28101  negsproplem6  28103  negbdaylem  28126  mulscom  28209  mulsass  28236  usgrfilem  29474  ex-dif  30571  shjcom  31507  indifundif  32672  imadifxp  32750  difioo  32934  nn0diffz0  32946  gsummulsubdishift1  33209  symgcom  33224  pmtrcnel2  33231  cycpmcl  33257  cycpm2tr  33260  tocyccntz  33285  lindsunlem  33882  lindsun  33883  fldext2rspun  33940  ordtcnvNEW  34178  xrge0iifcnv  34191  prsiga  34389  unelldsys  34416  measun  34469  measunl  34474  difelcarsg  34568  carsgclctunlem1  34575  carsggect  34576  eulerpartgbij  34630  circlemethhgt  34901  hgt750lemb  34914  bnj1416  35298  f1resfz0f1d  35428  subfacp1lem1  35493  subfacp1lem3  35496  pconnconn  35545  indispconn  35548  satfv1lem  35676  hfun  36492  onint1  36773  bj-fununsn2  37710  pibt2  37875  lindsenlbs  38078  poimirlem3  38086  poimirlem5  38088  poimirlem11  38094  poimirlem12  38095  poimirlem13  38096  poimirlem14  38097  poimirlem15  38098  poimirlem16  38099  poimirlem19  38102  poimirlem20  38103  poimirlem21  38104  poimirlem22  38105  poimirlem28  38111  poimirlem30  38113  ecuncnvepres  38858  padd02  40400  paddcom  40401  pclfinclN  40538  djhcom  41993  elrfi  43239  fzsplit1nn0  43299  eldioph2lem1  43305  eldioph2lem2  43306  diophin  43317  eldioph4b  43352  diophren  43354  kelac2  43606  pwssplit4  43630  iocunico  43752  rp-fakeuninass  44056  iunrelexp0  44242  corcltrcl  44279  frege124d  44301  mnuprdlem1  44812  equncomVD  45407  iunconnlem2  45474  snunioo1  46052  iccdifioo  46055  limciccioolb  46161  sumnnodd  46170  dirkercncflem2  46642  dirkercncflem3  46643  fourierdlem32  46677  fourierdlem93  46737  isomenndlem  47068  hoidmvlelem2  47134  hspmbllem1  47164  hspmbllem2  47165  fsumsplitsndif  47939  isubgr3stgrlem1  48552  usgrexmpl1edg  48610  usgrexmpl2edg  48615  aacllem  50386