Theorem uncom 4105

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

Syntax hints:   ∨ wo 847   = wceq 1541   ∈ wcel 2111   ∪ cun 3895

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 2113  ax-9 2121  ax-ext 2703

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 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-un 3902

This theorem is referenced by:  equncom  4106  uneq2  4109  un12  4120  un23  4121  ssun2  4126  unss2  4134  ssequn2  4136  symdifcom  4201  undir  4234  unineq  4235  dif32  4249  0un  4343  disjpss  4408  undif1  4423  undif2  4424  undifrOLD  4431  difcom  4436  uneqdifeq  4440  dfif4  4488  dfif5  4489  pwundif  4571  prcom  4682  tpass  4702  prprc1  4715  ssunsn2  4776  sspr  4784  sstp  4785  symdifv  5032  iunxdif3  5041  unidif0  5296  difxp2  6113  suc0  6383  fununfun  6529  fnunres2  6594  fresaunres2  6695  fresaunres1  6696  f1oprswap  6807  fvun2  6914  fvsnun2  7117  fsnunfv  7121  fveqf1o  7236  difex2  7693  elpwun  7702  fnsuppeq0  8122  oev2  8438  oacomf1o  8480  undifixp  8858  dfdom2  8900  domunsncan  8990  enfixsn  8999  domunsn  9040  limensuci  9066  findcard2  9074  findcard2s  9075  unfi  9080  ssfi  9082  enp1ilem  9162  frfi  9169  domunfican  9206  fsuppunbi  9273  elfiun  9314  infdifsn  9547  cantnfp1lem3  9570  rankmapu  9771  djuunxp  9814  infunsdom1  10103  infunsdom  10104  infxp  10105  ackbij1lem2  10111  ackbij1lem18  10127  fin1a2lem10  10300  fin1a2lem13  10303  zornn0g  10396  alephadd  10468  fpwwe2lem12  10533  canthp1lem1  10543  xrsupss  13208  xrinfmss  13209  supxrmnf  13216  prunioo  13381  fzsuc2  13482  fzdifsuc  13484  fseq1p1m1  13498  hashinf  14242  hashun3  14291  hashbclem  14359  relexpcnv  14942  fsumsplit1  15652  modfsummods  15700  incexclem  15743  lcmfunsnlem  16552  ramub1lem1  16938  setsid  17118  mreexexlem3d  17552  mreexexlem4d  17553  cnvtsr  18494  symgvalstruct  19309  gsumzaddlem  19833  gsummptfzsplitl  19845  dmdprdsplit2  19960  lspsnat  21082  lsppratlem3  21086  indistopon  22916  indistps  22926  indistps2  22927  ordtcnv  23116  leordtval2  23127  lecldbas  23134  cmpcld  23317  iunconn  23343  ufprim  23824  alexsubALTlem3  23964  ptcmplem1  23967  xpsdsval  24296  iccntr  24737  reconn  24744  volun  25473  voliunlem1  25478  icombl  25492  ioombl  25493  ismbf3d  25582  itgioo  25744  itgsplitioo  25766  lhop  25948  plyeq0  26143  fta1lem  26242  birthdaylem2  26889  lgsquadlem2  27319  nosepdm  27623  addscom  27909  addsproplem4  27915  addsproplem6  27917  negsproplem4  27973  negsproplem6  27975  negsbdaylem  27998  mulscom  28078  mulsass  28105  usgrfilem  29305  ex-dif  30403  shjcom  31338  indifundif  32504  imadifxp  32581  difioo  32765  symgcom  33052  pmtrcnel2  33059  cycpmcl  33085  cycpm2tr  33088  tocyccntz  33113  lindsunlem  33637  lindsun  33638  fldext2rspun  33695  ordtcnvNEW  33933  xrge0iifcnv  33946  prsiga  34144  unelldsys  34171  measun  34224  measunl  34229  difelcarsg  34323  carsgclctunlem1  34330  carsggect  34331  eulerpartgbij  34385  circlemethhgt  34656  hgt750lemb  34669  bnj1416  35051  f1resfz0f1d  35158  subfacp1lem1  35223  subfacp1lem3  35226  pconnconn  35275  indispconn  35278  satfv1lem  35406  hfun  36222  onint1  36493  bj-fununsn2  37298  pibt2  37461  lindsenlbs  37654  poimirlem3  37662  poimirlem5  37664  poimirlem11  37670  poimirlem12  37671  poimirlem13  37672  poimirlem14  37673  poimirlem15  37674  poimirlem16  37675  poimirlem19  37678  poimirlem20  37679  poimirlem21  37680  poimirlem22  37681  poimirlem28  37687  poimirlem30  37689  ecuncnvepres  38418  padd02  39910  paddcom  39911  pclfinclN  40048  djhcom  41503  elrfi  42786  fzsplit1nn0  42846  eldioph2lem1  42852  eldioph2lem2  42853  diophin  42864  eldioph4b  42903  diophren  42905  kelac2  43157  pwssplit4  43181  iocunico  43303  rp-fakeuninass  43608  iunrelexp0  43794  corcltrcl  43831  frege124d  43853  mnuprdlem1  44364  equncomVD  44959  iunconnlem2  45026  snunioo1  45611  iccdifioo  45614  limciccioolb  45720  sumnnodd  45729  dirkercncflem2  46201  dirkercncflem3  46202  fourierdlem32  46236  fourierdlem93  46296  isomenndlem  46627  hoidmvlelem2  46693  hspmbllem1  46723  hspmbllem2  46724  fsumsplitsndif  47472  isubgr3stgrlem1  48065  usgrexmpl1edg  48123  usgrexmpl2edg  48128  aacllem  49901