Theorem uncom 3908

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 859	. . 3 ⊢ ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) ↔ (𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐴))
2		elun 3904	. . 3 ⊢ (𝑥 ∈ (𝐵 ∪ 𝐴) ↔ (𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐴))
3	1, 2	bitr4i 267	. 2 ⊢ ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ (𝐵 ∪ 𝐴))
4	3	uneqri 3906	1 ⊢ (𝐴 ∪ 𝐵) = (𝐵 ∪ 𝐴)

Syntax hints:   ∨ wo 836   = wceq 1631   ∈ wcel 2145   ∪ cun 3721

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751

This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-v 3353  df-un 3728

This theorem is referenced by:  equncom  3909  uneq2  3912  un12  3922  un23  3923  ssun2  3928  unss2  3935  ssequn2  3937  symdifcom  3995  undir  4025  unineq  4026  dif32  4039  disjpss  4171  undif1  4185  undif2  4186  difcom  4195  uneqdifeq  4199  dfif4  4240  dfif5  4241  prcom  4403  tpass  4423  prprc1  4436  difsnid  4476  ssunsn2  4493  sspr  4499  sstp  4500  symdifv  4732  iunxdif3  4740  unidif0  4969  difxp2  5699  suc0  5940  fununfun  6075  fresaunres2  6214  fresaunres1  6215  f1oprswap  6319  fvun2  6410  fvsnun2  6591  fsnunfv  6595  fveqf1o  6698  difex2  7114  elpwun  7122  fnsuppeq0  7473  oev2  7755  oacomf1o  7797  ralxpmap  8059  undifixp  8096  dfdom2  8133  domunsncan  8214  enfixsn  8223  domunsn  8264  limensuci  8290  phplem2  8294  enp1ilem  8348  findcard2  8354  findcard2s  8355  frfi  8359  domunfican  8387  fsuppunbi  8450  elfiun  8490  infdifsn  8716  cantnfp1lem3  8739  rankmapu  8903  djuunxp  8945  cdacomen  9203  infunsdom1  9235  infunsdom  9236  infxp  9237  ackbij1lem2  9243  ackbij1lem18  9259  fin1a2lem10  9431  fin1a2lem13  9434  zornn0g  9527  alephadd  9599  fpwwe2lem13  9664  canthp1lem1  9674  xrsupss  12337  xrinfmss  12338  supxrmnf  12345  prunioo  12501  fzsuc2  12598  fzdifsuc  12600  fseq1p1m1  12614  hashinf  13319  hashun3  13368  hashbclem  13431  relexpcnv  13976  modfsummods  14725  incexclem  14768  lcmfunsnlem  15555  ramub1lem1  15930  setsid  16114  mreexexlem3d  16507  mreexexlem4d  16508  cnvtsr  17423  gsumzaddlem  18521  gsummptfzsplitl  18533  dmdprdsplit2  18646  lspsnat  19352  lsppratlem3  19357  indistopon  21019  indistps  21029  indistps2  21030  ordtcnv  21219  leordtval2  21230  lecldbas  21237  cmpcld  21419  iunconn  21445  ufprim  21926  alexsubALTlem3  22066  ptcmplem1  22069  xpsdsval  22399  iccntr  22837  reconn  22844  volun  23526  voliunlem1  23531  icombl  23545  ioombl  23546  ismbf3d  23634  itgioo  23795  itgsplitioo  23817  lhop  23992  plyeq0  24180  fta1lem  24275  birthdaylem2  24893  lgsquadlem2  25320  usgrfilem  26435  ex-dif  27615  shjcom  28550  indifundif  29687  imadifxp  29745  difioo  29877  ordtcnvNEW  30299  xrge0iifcnv  30312  prsiga  30527  unelldsys  30554  measun  30607  measunl  30612  difelcarsg  30705  carsgclctunlem1  30712  carsggect  30713  eulerpartgbij  30767  circlemethhgt  31054  hgt750lemb  31067  bnj1416  31438  subfacp1lem1  31492  subfacp1lem3  31495  pconnconn  31544  indispconn  31547  nosepdm  32164  hfun  32615  onint1  32778  bj-pr22val  33331  lindsenlbs  33730  poimirlem3  33738  poimirlem5  33740  poimirlem11  33746  poimirlem12  33747  poimirlem13  33748  poimirlem14  33749  poimirlem15  33750  poimirlem16  33751  poimirlem19  33754  poimirlem20  33755  poimirlem21  33756  poimirlem22  33757  poimirlem28  33763  poimirlem30  33765  padd02  35613  paddcom  35614  pclfinclN  35751  djhcom  37208  elrfi  37776  fzsplit1nn0  37836  eldioph2lem1  37842  eldioph2lem2  37843  diophin  37855  eldioph4b  37894  diophren  37896  kelac2  38154  pwssplit4  38178  iocunico  38315  rp-fakeuninass  38381  iunrelexp0  38513  corcltrcl  38550  frege124d  38572  equncomVD  39619  iunconnlem2  39686  0un  39729  snunioo1  40250  iccdifioo  40253  fsumsplit1  40315  limciccioolb  40364  sumnnodd  40373  dirkercncflem2  40831  dirkercncflem3  40832  fourierdlem32  40866  fourierdlem93  40926  prsal  41048  isomenndlem  41257  hoidmvlelem2  41323  hspmbllem1  41353  hspmbllem2  41354  fsumsplitsndif  41864  aacllem  43071