Theorem uncom 4108

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

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

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 3907

This theorem is referenced by:  equncom  4109  uneq2  4112  un12  4123  un23  4124  ssun2  4129  unss2  4137  ssequn2  4139  symdifcom  4204  undir  4237  unineq  4238  dif32  4252  0un  4346  disjpss  4411  undif1  4426  undif2  4427  undifrOLD  4434  difcom  4439  uneqdifeq  4443  dfif4  4491  dfif5  4492  pwundif  4574  prcom  4685  tpass  4705  prprc1  4718  ssunsn2  4779  sspr  4787  sstp  4788  symdifv  5034  iunxdif3  5043  unidif0  5298  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  19310  gsumzaddlem  19834  gsummptfzsplitl  19846  dmdprdsplit2  19961  lspsnat  21083  lsppratlem3  21087  indistopon  22917  indistps  22927  indistps2  22928  ordtcnv  23117  leordtval2  23128  lecldbas  23135  cmpcld  23318  iunconn  23344  ufprim  23825  alexsubALTlem3  23965  ptcmplem1  23968  xpsdsval  24297  iccntr  24738  reconn  24745  volun  25474  voliunlem1  25479  icombl  25493  ioombl  25494  ismbf3d  25583  itgioo  25745  itgsplitioo  25767  lhop  25949  plyeq0  26144  fta1lem  26243  birthdaylem2  26890  lgsquadlem2  27320  nosepdm  27624  addscom  27910  addsproplem4  27916  addsproplem6  27918  negsproplem4  27974  negsproplem6  27976  negsbdaylem  27999  mulscom  28079  mulsass  28106  usgrfilem  29306  ex-dif  30401  shjcom  31336  indifundif  32502  imadifxp  32579  difioo  32763  symgcom  33050  pmtrcnel2  33057  cycpmcl  33083  cycpm2tr  33086  tocyccntz  33111  lindsunlem  33635  lindsun  33636  fldext2rspun  33693  ordtcnvNEW  33931  xrge0iifcnv  33944  prsiga  34142  unelldsys  34169  measun  34222  measunl  34227  difelcarsg  34321  carsgclctunlem1  34328  carsggect  34329  eulerpartgbij  34383  circlemethhgt  34654  hgt750lemb  34667  bnj1416  35049  f1resfz0f1d  35156  subfacp1lem1  35221  subfacp1lem3  35224  pconnconn  35273  indispconn  35276  satfv1lem  35404  hfun  36218  onint1  36489  bj-fununsn2  37294  pibt2  37457  lindsenlbs  37661  poimirlem3  37669  poimirlem5  37671  poimirlem11  37677  poimirlem12  37678  poimirlem13  37679  poimirlem14  37680  poimirlem15  37681  poimirlem16  37682  poimirlem19  37685  poimirlem20  37686  poimirlem21  37687  poimirlem22  37688  poimirlem28  37694  poimirlem30  37696  padd02  39857  paddcom  39858  pclfinclN  39995  djhcom  41450  elrfi  42733  fzsplit1nn0  42793  eldioph2lem1  42799  eldioph2lem2  42800  diophin  42811  eldioph4b  42850  diophren  42852  kelac2  43104  pwssplit4  43128  iocunico  43250  rp-fakeuninass  43555  iunrelexp0  43741  corcltrcl  43778  frege124d  43800  mnuprdlem1  44311  equncomVD  44906  iunconnlem2  44973  snunioo1  45558  iccdifioo  45561  limciccioolb  45667  sumnnodd  45676  dirkercncflem2  46148  dirkercncflem3  46149  fourierdlem32  46183  fourierdlem93  46243  isomenndlem  46574  hoidmvlelem2  46640  hspmbllem1  46670  hspmbllem2  46671  fsumsplitsndif  47410  isubgr3stgrlem1  48003  usgrexmpl1edg  48061  usgrexmpl2edg  48066  aacllem  49839