Theorem uncom 4099

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

Syntax hints:   ∨ wo 848   = wceq 1542   ∈ wcel 2114   ∪ cun 3888

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3432  df-un 3895

This theorem is referenced by:  equncom  4100  uneq2  4103  un12  4114  un23  4115  ssun2  4120  unss2  4128  ssequn2  4130  symdifcom  4195  undir  4228  unineq  4229  dif32  4243  0un  4337  disjpss  4402  undif1  4417  undif2  4418  difcom  4429  uneqdifeq  4433  dfif4  4483  dfif5  4484  pwundif  4566  prcom  4677  tpass  4697  prprc1  4710  ssunsn2  4771  sstp  4780  unidif0  5297  difxp2  6124  suc0  6394  fununfun  6540  fnunres2  6605  fresaunres2  6706  fresaunres1  6707  f1oprswap  6819  fvun2  6926  fvsnun2  7131  fsnunfv  7135  fveqf1o  7250  difex2  7707  elpwun  7716  fnsuppeq0  8135  oev2  8451  oacomf1o  8493  undifixp  8875  dfdom2  8918  domunsncan  9008  enfixsn  9017  domunsn  9058  limensuci  9084  findcard2  9092  findcard2s  9093  unfi  9098  ssfi  9100  enp1ilem  9181  frfi  9188  domunfican  9225  fsuppunbi  9295  elfiun  9336  infdifsn  9569  cantnfp1lem3  9592  rankmapu  9793  djuunxp  9836  infunsdom1  10125  infunsdom  10126  infxp  10127  ackbij1lem2  10133  ackbij1lem18  10149  fin1a2lem10  10322  fin1a2lem13  10325  zornn0g  10418  alephadd  10491  fpwwe2lem12  10556  canthp1lem1  10566  xrsupss  13252  xrinfmss  13253  supxrmnf  13260  prunioo  13425  fzsuc2  13527  fzdifsuc  13529  fseq1p1m1  13543  hashinf  14288  hashun3  14337  hashbclem  14405  relexpcnv  14988  fsumsplit1  15698  modfsummods  15747  incexclem  15792  lcmfunsnlem  16601  ramub1lem1  16988  setsid  17168  mreexexlem3d  17603  mreexexlem4d  17604  cnvtsr  18545  symgvalstruct  19363  gsumzaddlem  19887  gsummptfzsplitl  19899  dmdprdsplit2  20014  lspsnat  21135  lsppratlem3  21139  indistopon  22976  indistps  22986  indistps2  22987  ordtcnv  23176  leordtval2  23187  lecldbas  23194  cmpcld  23377  iunconn  23403  ufprim  23884  alexsubALTlem3  24024  ptcmplem1  24027  xpsdsval  24356  iccntr  24797  reconn  24804  volun  25522  voliunlem1  25527  icombl  25541  ioombl  25542  ismbf3d  25631  itgioo  25793  itgsplitioo  25815  lhop  25993  plyeq0  26186  fta1lem  26284  birthdaylem2  26929  lgsquadlem2  27358  nosepdm  27662  addscom  27972  addsproplem4  27978  addsproplem6  27980  negsproplem4  28037  negsproplem6  28039  negbdaylem  28062  mulscom  28145  mulsass  28172  usgrfilem  29410  ex-dif  30508  shjcom  31444  indifundif  32609  imadifxp  32686  difioo  32870  nn0diffz0  32882  gsummulsubdishift1  33144  symgcom  33159  pmtrcnel2  33166  cycpmcl  33192  cycpm2tr  33195  tocyccntz  33220  lindsunlem  33784  lindsun  33785  fldext2rspun  33842  ordtcnvNEW  34080  xrge0iifcnv  34093  prsiga  34291  unelldsys  34318  measun  34371  measunl  34376  difelcarsg  34470  carsgclctunlem1  34477  carsggect  34478  eulerpartgbij  34532  circlemethhgt  34803  hgt750lemb  34816  bnj1416  35197  f1resfz0f1d  35312  subfacp1lem1  35377  subfacp1lem3  35380  pconnconn  35429  indispconn  35432  satfv1lem  35560  hfun  36376  onint1  36647  bj-fununsn2  37584  pibt2  37747  lindsenlbs  37950  poimirlem3  37958  poimirlem5  37960  poimirlem11  37966  poimirlem12  37967  poimirlem13  37968  poimirlem14  37969  poimirlem15  37970  poimirlem16  37971  poimirlem19  37974  poimirlem20  37975  poimirlem21  37976  poimirlem22  37977  poimirlem28  37983  poimirlem30  37985  ecuncnvepres  38730  padd02  40272  paddcom  40273  pclfinclN  40410  djhcom  41865  elrfi  43140  fzsplit1nn0  43200  eldioph2lem1  43206  eldioph2lem2  43207  diophin  43218  eldioph4b  43257  diophren  43259  kelac2  43511  pwssplit4  43535  iocunico  43657  rp-fakeuninass  43961  iunrelexp0  44147  corcltrcl  44184  frege124d  44206  mnuprdlem1  44717  equncomVD  45312  iunconnlem2  45379  snunioo1  45960  iccdifioo  45963  limciccioolb  46069  sumnnodd  46078  dirkercncflem2  46550  dirkercncflem3  46551  fourierdlem32  46585  fourierdlem93  46645  isomenndlem  46976  hoidmvlelem2  47042  hspmbllem1  47072  hspmbllem2  47073  fsumsplitsndif  47841  isubgr3stgrlem1  48454  usgrexmpl1edg  48512  usgrexmpl2edg  48517  aacllem  50288