Theorem uncom 4111

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

Syntax hints:   ∨ wo 847   = wceq 1540   ∈ wcel 2109   ∪ cun 3903

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 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3440  df-un 3910

This theorem is referenced by:  equncom  4112  uneq2  4115  un12  4126  un23  4127  ssun2  4132  unss2  4140  ssequn2  4142  symdifcom  4207  undir  4240  unineq  4241  dif32  4255  0un  4349  disjpss  4414  undif1  4429  undif2  4430  undifrOLD  4437  difcom  4442  uneqdifeq  4446  dfif4  4494  dfif5  4495  pwundif  4577  prcom  4686  tpass  4706  prprc1  4719  ssunsn2  4781  sspr  4789  sstp  4790  symdifv  5038  iunxdif3  5047  unidif0  5302  difxp2  6119  suc0  6388  fununfun  6534  fnunres2  6599  fresaunres2  6700  fresaunres1  6701  f1oprswap  6812  fvun2  6919  fvsnun2  7123  fsnunfv  7127  fveqf1o  7243  difex2  7700  elpwun  7709  fnsuppeq0  8132  oev2  8448  oacomf1o  8490  undifixp  8868  dfdom2  8910  domunsncan  9001  enfixsn  9010  domunsn  9051  limensuci  9077  findcard2  9088  findcard2s  9089  unfi  9095  ssfi  9097  enp1ilem  9181  frfi  9190  domunfican  9230  fsuppunbi  9298  elfiun  9339  infdifsn  9572  cantnfp1lem3  9595  rankmapu  9793  djuunxp  9836  infunsdom1  10125  infunsdom  10126  infxp  10127  ackbij1lem2  10133  ackbij1lem18  10149  fin1a2lem10  10322  fin1a2lem13  10325  zornn0g  10418  alephadd  10490  fpwwe2lem12  10555  canthp1lem1  10565  xrsupss  13229  xrinfmss  13230  supxrmnf  13237  prunioo  13402  fzsuc2  13503  fzdifsuc  13505  fseq1p1m1  13519  hashinf  14260  hashun3  14309  hashbclem  14377  relexpcnv  14960  fsumsplit1  15670  modfsummods  15718  incexclem  15761  lcmfunsnlem  16570  ramub1lem1  16956  setsid  17136  mreexexlem3d  17570  mreexexlem4d  17571  cnvtsr  18512  symgvalstruct  19294  gsumzaddlem  19818  gsummptfzsplitl  19830  dmdprdsplit2  19945  lspsnat  21070  lsppratlem3  21074  indistopon  22904  indistps  22914  indistps2  22915  ordtcnv  23104  leordtval2  23115  lecldbas  23122  cmpcld  23305  iunconn  23331  ufprim  23812  alexsubALTlem3  23952  ptcmplem1  23955  xpsdsval  24285  iccntr  24726  reconn  24733  volun  25462  voliunlem1  25467  icombl  25481  ioombl  25482  ismbf3d  25571  itgioo  25733  itgsplitioo  25755  lhop  25937  plyeq0  26132  fta1lem  26231  birthdaylem2  26878  lgsquadlem2  27308  nosepdm  27612  addscom  27896  addsproplem4  27902  addsproplem6  27904  negsproplem4  27960  negsproplem6  27962  negsbdaylem  27985  mulscom  28065  mulsass  28092  usgrfilem  29290  ex-dif  30385  shjcom  31320  indifundif  32486  imadifxp  32563  difioo  32738  symgcom  33038  pmtrcnel2  33045  cycpmcl  33071  cycpm2tr  33074  tocyccntz  33099  lindsunlem  33599  lindsun  33600  fldext2rspun  33656  ordtcnvNEW  33889  xrge0iifcnv  33902  prsiga  34100  unelldsys  34127  measun  34180  measunl  34185  difelcarsg  34280  carsgclctunlem1  34287  carsggect  34288  eulerpartgbij  34342  circlemethhgt  34613  hgt750lemb  34626  bnj1416  35008  f1resfz0f1d  35089  subfacp1lem1  35154  subfacp1lem3  35157  pconnconn  35206  indispconn  35209  satfv1lem  35337  hfun  36154  onint1  36425  bj-fununsn2  37230  pibt2  37393  lindsenlbs  37597  poimirlem3  37605  poimirlem5  37607  poimirlem11  37613  poimirlem12  37614  poimirlem13  37615  poimirlem14  37616  poimirlem15  37617  poimirlem16  37618  poimirlem19  37621  poimirlem20  37622  poimirlem21  37623  poimirlem22  37624  poimirlem28  37630  poimirlem30  37632  padd02  39794  paddcom  39795  pclfinclN  39932  djhcom  41387  elrfi  42670  fzsplit1nn0  42730  eldioph2lem1  42736  eldioph2lem2  42737  diophin  42748  eldioph4b  42787  diophren  42789  kelac2  43041  pwssplit4  43065  iocunico  43187  rp-fakeuninass  43492  iunrelexp0  43678  corcltrcl  43715  frege124d  43737  mnuprdlem1  44248  equncomVD  44844  iunconnlem2  44911  snunioo1  45497  iccdifioo  45500  limciccioolb  45606  sumnnodd  45615  dirkercncflem2  46089  dirkercncflem3  46090  fourierdlem32  46124  fourierdlem93  46184  isomenndlem  46515  hoidmvlelem2  46581  hspmbllem1  46611  hspmbllem2  46612  fsumsplitsndif  47361  isubgr3stgrlem1  47954  usgrexmpl1edg  48012  usgrexmpl2edg  48017  aacllem  49790