Theorem uncom 4110

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 870	. . 3 ⊢ ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) ↔ (𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐴))
2		elun 4105	. . 3 ⊢ (𝑥 ∈ (𝐵 ∪ 𝐴) ↔ (𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐴))
3	1, 2	bitr4i 278	. 2 ⊢ ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ (𝐵 ∪ 𝐴))
4	3	uneqri 4108	1 ⊢ (𝐴 ∪ 𝐵) = (𝐵 ∪ 𝐴)

Syntax hints:   ∨ wo 847   = wceq 1541   ∈ wcel 2113   ∪ cun 3899

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-un 3906

This theorem is referenced by:  equncom  4111  uneq2  4114  un12  4125  un23  4126  ssun2  4131  unss2  4139  ssequn2  4141  symdifcom  4206  undir  4239  unineq  4240  dif32  4254  0un  4348  disjpss  4413  undif1  4428  undif2  4429  undifrOLD  4436  difcom  4441  uneqdifeq  4445  dfif4  4495  dfif5  4496  pwundif  4578  prcom  4689  tpass  4709  prprc1  4722  ssunsn2  4783  sspr  4791  sstp  4792  symdifv  5041  iunxdif3  5050  unidif0  5305  difxp2  6124  suc0  6394  fununfun  6540  fnunres2  6605  fresaunres2  6706  fresaunres1  6707  f1oprswap  6819  fvun2  6926  fvsnun2  7129  fsnunfv  7133  fveqf1o  7248  difex2  7705  elpwun  7714  fnsuppeq0  8134  oev2  8450  oacomf1o  8492  undifixp  8872  dfdom2  8915  domunsncan  9005  enfixsn  9014  domunsn  9055  limensuci  9081  findcard2  9089  findcard2s  9090  unfi  9095  ssfi  9097  enp1ilem  9178  frfi  9185  domunfican  9222  fsuppunbi  9292  elfiun  9333  infdifsn  9566  cantnfp1lem3  9589  rankmapu  9790  djuunxp  9833  infunsdom1  10122  infunsdom  10123  infxp  10124  ackbij1lem2  10130  ackbij1lem18  10146  fin1a2lem10  10319  fin1a2lem13  10322  zornn0g  10415  alephadd  10488  fpwwe2lem12  10553  canthp1lem1  10563  xrsupss  13224  xrinfmss  13225  supxrmnf  13232  prunioo  13397  fzsuc2  13498  fzdifsuc  13500  fseq1p1m1  13514  hashinf  14258  hashun3  14307  hashbclem  14375  relexpcnv  14958  fsumsplit1  15668  modfsummods  15716  incexclem  15759  lcmfunsnlem  16568  ramub1lem1  16954  setsid  17134  mreexexlem3d  17569  mreexexlem4d  17570  cnvtsr  18511  symgvalstruct  19326  gsumzaddlem  19850  gsummptfzsplitl  19862  dmdprdsplit2  19977  lspsnat  21100  lsppratlem3  21104  indistopon  22945  indistps  22955  indistps2  22956  ordtcnv  23145  leordtval2  23156  lecldbas  23163  cmpcld  23346  iunconn  23372  ufprim  23853  alexsubALTlem3  23993  ptcmplem1  23996  xpsdsval  24325  iccntr  24766  reconn  24773  volun  25502  voliunlem1  25507  icombl  25521  ioombl  25522  ismbf3d  25611  itgioo  25773  itgsplitioo  25795  lhop  25977  plyeq0  26172  fta1lem  26271  birthdaylem2  26918  lgsquadlem2  27348  nosepdm  27652  addscom  27962  addsproplem4  27968  addsproplem6  27970  negsproplem4  28027  negsproplem6  28029  negbdaylem  28052  mulscom  28135  mulsass  28162  usgrfilem  29400  ex-dif  30498  shjcom  31433  indifundif  32599  imadifxp  32676  difioo  32862  nn0diffz0  32874  gsummulsubdishift1  33151  symgcom  33165  pmtrcnel2  33172  cycpmcl  33198  cycpm2tr  33201  tocyccntz  33226  lindsunlem  33781  lindsun  33782  fldext2rspun  33839  ordtcnvNEW  34077  xrge0iifcnv  34090  prsiga  34288  unelldsys  34315  measun  34368  measunl  34373  difelcarsg  34467  carsgclctunlem1  34474  carsggect  34475  eulerpartgbij  34529  circlemethhgt  34800  hgt750lemb  34813  bnj1416  35195  f1resfz0f1d  35308  subfacp1lem1  35373  subfacp1lem3  35376  pconnconn  35425  indispconn  35428  satfv1lem  35556  hfun  36372  onint1  36643  bj-fununsn2  37459  pibt2  37622  lindsenlbs  37816  poimirlem3  37824  poimirlem5  37826  poimirlem11  37832  poimirlem12  37833  poimirlem13  37834  poimirlem14  37835  poimirlem15  37836  poimirlem16  37837  poimirlem19  37840  poimirlem20  37841  poimirlem21  37842  poimirlem22  37843  poimirlem28  37849  poimirlem30  37851  ecuncnvepres  38580  padd02  40072  paddcom  40073  pclfinclN  40210  djhcom  41665  elrfi  42936  fzsplit1nn0  42996  eldioph2lem1  43002  eldioph2lem2  43003  diophin  43014  eldioph4b  43053  diophren  43055  kelac2  43307  pwssplit4  43331  iocunico  43453  rp-fakeuninass  43757  iunrelexp0  43943  corcltrcl  43980  frege124d  44002  mnuprdlem1  44513  equncomVD  45108  iunconnlem2  45175  snunioo1  45758  iccdifioo  45761  limciccioolb  45867  sumnnodd  45876  dirkercncflem2  46348  dirkercncflem3  46349  fourierdlem32  46383  fourierdlem93  46443  isomenndlem  46774  hoidmvlelem2  46840  hspmbllem1  46870  hspmbllem2  46871  fsumsplitsndif  47619  isubgr3stgrlem1  48212  usgrexmpl1edg  48270  usgrexmpl2edg  48275  aacllem  50046