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

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

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-un 3904

This theorem is used by:  equncom  4106  uneq2  4109  un12  4119  un23  4120  ssun2  4125  unss2  4133  ssequn2  4135  symdifcom  4200  undir  4233  unineq  4234  dif32  4248  0un  4346  disjpss  4414  undif1  4430  undif2  4431  difcom  4444  uneqdifeq  4448  dfif4  4498  dfif5  4499  pwundif  4582  prcom  4693  tpass  4713  prprc1  4726  ssunsn2  4788  sstp  4796  unidif0OLD  5322  difxp2  6156  suc0  6433  fununfun  6580  fnunres2  6644  fresaunres2  6746  fresaunres1  6747  f1oprswap  6862  fvun2  6969  fvsnun2  7180  fsnunfv  7184  fveqf1o  7302  difex2  7763  elpwun  7772  fnsuppeq0  8193  oev2  8515  oacomf1o  8557  undifixp  8946  dfdom2  8989  domunsncan  9080  enfixsn  9089  domunsn  9130  limensuci  9156  findcard2  9164  findcard2s  9165  unfi  9170  ssfi  9172  enp1ilem  9253  frfi  9260  domunfican  9297  fsuppunbi  9365  elfiun  9406  infdifsn  9642  cantnfp1lem3  9665  rankmapu  9876  hfunOLD  9900  djuunxp  9983  infunsdom1  10271  infunsdom  10272  infxp  10273  ackbij1lem2  10279  ackbij1lem18  10295  fin1a2lem10  10468  fin1a2lem13  10471  zornn0g  10564  alephadd  10643  fpwwe2lem12  10708  canthp1lem1  10718  xrsupss  13420  xrinfmss  13421  supxrmnf  13428  prunioo  13593  fzsuc2  13696  fzdifsuc  13698  fseq1p1m1  13712  f1resfz0f1d  13907  hashinf  14459  hashun3  14508  hashbclem  14577  relexpcnv  15168  fsumsplit1  15891  modfsummods  15940  incexclem  15985  lcmfunsnlem  16796  ramub1lem1  17184  setsid  17365  mreexexlem3d  17800  mreexexlem4d  17801  cnvtsr  18742  symgvalstruct  19591  gsumzaddlem  20115  gsummptfzsplitl  20127  dmdprdsplit2  20242  lspsnat  21403  lsppratlem3  21407  lindsenlbs  22137  indistopon  23299  indistps  23309  indistps2  23310  ordtcnv  23499  leordtval2  23510  lecldbas  23517  cmpcld  23700  iunconn  23726  ufprim  24208  alexsubALTlem3  24348  ptcmplem1  24351  xpsdsval  24680  iccntr  25121  reconn  25128  volun  25846  voliunlem1  25851  icombl  25865  ioombl  25866  ismbf3d  25955  itgioo  26116  itgsplitioo  26138  lhop  26316  plyeq0  26510  fta1lem  26610  birthdaylem2  27262  lgsquadlem2  27690  nosepdm  28023  addscom  28334  addsproplem4  28340  addsproplem6  28342  negsproplem4  28399  negsproplem6  28401  negbdaylem  28424  mulscom  28507  mulsass  28534  usgrfilem  29890  ex-dif  31006  shjcom  31942  indifundif  33102  imadifxp  33177  difioo  33356  nn0diffz0  33368  gsummulsubdishift1  33611  symgcom  33626  pmtrcnel2  33633  cycpmcl  33659  cycpm2tr  33662  tocyccntz  33687  lindsunlem  34238  lindsun  34239  fldext2rspun  34296  ordtcnvNEW  34534  xrge0iifcnv  34547  prsiga  34745  unelldsys  34773  measun  34826  measunl  34831  difelcarsg  34925  carsgclctunlem1  34932  carsggect  34933  eulerpartgbij  34987  circlemethhgt  35255  hgt750lemb  35268  bnj1416  35652  subfacp1lem1  35913  subfacp1lem3  35916  pconnconn  35965  indispconn  35968  satfv1lem  36096  onint1  37207  bj-fununsn2  38143  pibt2  38308  poimirlem3  38509  poimirlem5  38511  poimirlem11  38517  poimirlem12  38518  poimirlem13  38519  poimirlem14  38520  poimirlem15  38521  poimirlem16  38522  poimirlem19  38525  poimirlem20  38526  poimirlem21  38527  poimirlem22  38528  poimirlem28  38534  poimirlem30  38536  ecuncnvepres  39295  padd02  40837  paddcom  40838  pclfinclN  40975  djhcom  42430  elrfi  43658  fzsplit1nn0  43718  eldioph2lem1  43724  eldioph2lem2  43725  diophin  43736  eldioph4b  43771  diophren  43773  kelac2  44025  pwssplit4  44049  iocunico  44171  rp-fakeuninass  44475  iunrelexp0  44661  corcltrcl  44698  frege124d  44720  mnuprdlem1  45215  equncomVD  45809  iunconnlem2  45876  snunioo1  46468  iccdifioo  46471  limciccioolb  46577  sumnnodd  46586  dirkercncflem2  47058  dirkercncflem3  47059  fourierdlem32  47093  fourierdlem93  47153  isomenndlem  47484  hoidmvlelem2  47550  hspmbllem1  47580  hspmbllem2  47581  fsumsplitsndif  48395  isubgr3stgrlem1  49008  usgrexmpl1edg  49066  usgrexmpl2edg  49071  aacllem  50883