Theorem uncom 4122

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

Syntax hints:   ∨ wo 843   = wceq 1536   ∈ wcel 2113   ∪ cun 3927

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2160  ax-12 2176  ax-ext 2792

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1539  df-ex 1780  df-nf 1784  df-sb 2069  df-clab 2799  df-cleq 2813  df-clel 2892  df-nfc 2962  df-v 3493  df-un 3934

This theorem is referenced by:  equncom  4123  uneq2  4126  un12  4136  un23  4137  ssun2  4142  unss2  4150  ssequn2  4152  symdifcom  4213  undir  4246  unineq  4247  dif32  4260  0un  4339  disjpss  4403  undif1  4417  undif2  4418  difcom  4427  uneqdifeq  4431  dfif4  4475  dfif5  4476  pwundif  4558  prcom  4661  tpass  4681  prprc1  4694  difsnid  4736  ssunsn2  4753  sspr  4759  sstp  4760  symdifv  5001  iunxdif3  5010  unidif0  5253  difxp2  6016  suc0  6258  fununfun  6395  fresaunres2  6543  fresaunres1  6544  f1oprswap  6651  fvun2  6748  fvsnun2  6938  fsnunfv  6942  fveqf1o  7051  difex2  7475  elpwun  7484  fnsuppeq0  7851  oev2  8141  oacomf1o  8184  ralxpmap  8453  undifixp  8491  dfdom2  8528  domunsncan  8610  enfixsn  8619  domunsn  8660  limensuci  8686  phplem2  8690  enp1ilem  8745  findcard2  8751  findcard2s  8752  frfi  8756  domunfican  8784  fsuppunbi  8847  elfiun  8887  infdifsn  9113  cantnfp1lem3  9136  rankmapu  9300  djuunxp  9343  infunsdom1  9628  infunsdom  9629  infxp  9630  ackbij1lem2  9636  ackbij1lem18  9652  fin1a2lem10  9824  fin1a2lem13  9827  zornn0g  9920  alephadd  9992  fpwwe2lem13  10057  canthp1lem1  10067  xrsupss  12696  xrinfmss  12697  supxrmnf  12704  prunioo  12863  fzsuc2  12962  fzdifsuc  12964  fseq1p1m1  12978  hashinf  13692  hashun3  13742  hashbclem  13807  relexpcnv  14389  modfsummods  15143  incexclem  15186  lcmfunsnlem  15980  ramub1lem1  16357  setsid  16533  mreexexlem3d  16912  mreexexlem4d  16913  cnvtsr  17827  symgvalstruct  18520  gsumzaddlem  19036  gsummptfzsplitl  19048  dmdprdsplit2  19163  lspsnat  19912  lsppratlem3  19916  indistopon  21604  indistps  21614  indistps2  21615  ordtcnv  21804  leordtval2  21815  lecldbas  21822  cmpcld  22005  iunconn  22031  ufprim  22512  alexsubALTlem3  22652  ptcmplem1  22655  xpsdsval  22986  iccntr  23424  reconn  23431  volun  24141  voliunlem1  24146  icombl  24160  ioombl  24161  ismbf3d  24250  itgioo  24411  itgsplitioo  24433  lhop  24610  plyeq0  24799  fta1lem  24894  birthdaylem2  25528  lgsquadlem2  25955  usgrfilem  27107  ex-dif  28200  shjcom  29133  undifr  30284  indifundif  30285  imadifxp  30351  fnunres2  30424  difioo  30505  symgcom  30748  pmtrcnel2  30755  cycpmcl  30779  cycpm2tr  30782  tocyccntz  30807  lindsunlem  31044  lindsun  31045  ordtcnvNEW  31184  xrge0iifcnv  31197  prsiga  31411  unelldsys  31438  measun  31491  measunl  31496  difelcarsg  31589  carsgclctunlem1  31596  carsggect  31597  eulerpartgbij  31651  circlemethhgt  31935  hgt750lemb  31948  bnj1416  32332  f1resfz0f1d  32382  subfacp1lem1  32447  subfacp1lem3  32450  pconnconn  32499  indispconn  32502  satfv1lem  32630  nosepdm  33209  hfun  33660  onint1  33818  bj-fununsn2  34560  pibt2  34722  lindsenlbs  34922  poimirlem3  34930  poimirlem5  34932  poimirlem11  34938  poimirlem12  34939  poimirlem13  34940  poimirlem14  34941  poimirlem15  34942  poimirlem16  34943  poimirlem19  34946  poimirlem20  34947  poimirlem21  34948  poimirlem22  34949  poimirlem28  34955  poimirlem30  34957  padd02  36981  paddcom  36982  pclfinclN  37119  djhcom  38574  elrfi  39367  fzsplit1nn0  39427  eldioph2lem1  39433  eldioph2lem2  39434  diophin  39445  eldioph4b  39484  diophren  39486  kelac2  39741  pwssplit4  39765  iocunico  39893  rp-fakeuninass  39956  iunrelexp0  40121  corcltrcl  40158  frege124d  40180  mnuprdlem1  40682  equncomVD  41276  iunconnlem2  41343  snunioo1  41862  iccdifioo  41865  fsumsplit1  41927  limciccioolb  41976  sumnnodd  41985  dirkercncflem2  42463  dirkercncflem3  42464  fourierdlem32  42498  fourierdlem93  42558  isomenndlem  42886  hoidmvlelem2  42952  hspmbllem1  42982  hspmbllem2  42983  fsumsplitsndif  43607  aacllem  44976