Theorem uncom 4121

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

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

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 3449  df-un 3919

This theorem is referenced by:  equncom  4122  uneq2  4125  un12  4136  un23  4137  ssun2  4142  unss2  4150  ssequn2  4152  symdifcom  4217  undir  4250  unineq  4251  dif32  4265  0un  4359  disjpss  4424  undif1  4439  undif2  4440  undifrOLD  4447  difcom  4452  uneqdifeq  4456  dfif4  4504  dfif5  4505  pwundif  4587  prcom  4696  tpass  4716  prprc1  4729  ssunsn2  4791  sspr  4799  sstp  4800  symdifv  5050  iunxdif3  5059  unidif0  5315  difxp2  6139  suc0  6409  fununfun  6564  fnunres2  6631  fresaunres2  6732  fresaunres1  6733  f1oprswap  6844  fvun2  6953  fvsnun2  7157  fsnunfv  7161  fveqf1o  7277  difex2  7736  elpwun  7745  fnsuppeq0  8171  oev2  8487  oacomf1o  8529  undifixp  8907  dfdom2  8949  domunsncan  9041  enfixsn  9050  domunsn  9091  limensuci  9117  findcard2  9128  findcard2s  9129  unfi  9135  ssfi  9137  enp1ilem  9223  frfi  9232  domunfican  9272  fsuppunbi  9340  elfiun  9381  infdifsn  9610  cantnfp1lem3  9633  rankmapu  9831  djuunxp  9874  infunsdom1  10165  infunsdom  10166  infxp  10167  ackbij1lem2  10173  ackbij1lem18  10189  fin1a2lem10  10362  fin1a2lem13  10365  zornn0g  10458  alephadd  10530  fpwwe2lem12  10595  canthp1lem1  10605  xrsupss  13269  xrinfmss  13270  supxrmnf  13277  prunioo  13442  fzsuc2  13543  fzdifsuc  13545  fseq1p1m1  13559  hashinf  14300  hashun3  14349  hashbclem  14417  relexpcnv  15001  fsumsplit1  15711  modfsummods  15759  incexclem  15802  lcmfunsnlem  16611  ramub1lem1  16997  setsid  17177  mreexexlem3d  17607  mreexexlem4d  17608  cnvtsr  18547  symgvalstruct  19327  gsumzaddlem  19851  gsummptfzsplitl  19863  dmdprdsplit2  19978  lspsnat  21055  lsppratlem3  21059  indistopon  22888  indistps  22898  indistps2  22899  ordtcnv  23088  leordtval2  23099  lecldbas  23106  cmpcld  23289  iunconn  23315  ufprim  23796  alexsubALTlem3  23936  ptcmplem1  23939  xpsdsval  24269  iccntr  24710  reconn  24717  volun  25446  voliunlem1  25451  icombl  25465  ioombl  25466  ismbf3d  25555  itgioo  25717  itgsplitioo  25739  lhop  25921  plyeq0  26116  fta1lem  26215  birthdaylem2  26862  lgsquadlem2  27292  nosepdm  27596  addscom  27873  addsproplem4  27879  addsproplem6  27881  negsproplem4  27937  negsproplem6  27939  negsbdaylem  27962  mulscom  28042  mulsass  28069  usgrfilem  29254  ex-dif  30352  shjcom  31287  indifundif  32453  imadifxp  32530  difioo  32705  symgcom  33040  pmtrcnel2  33047  cycpmcl  33073  cycpm2tr  33076  tocyccntz  33101  lindsunlem  33620  lindsun  33621  fldext2rspun  33677  ordtcnvNEW  33910  xrge0iifcnv  33923  prsiga  34121  unelldsys  34148  measun  34201  measunl  34206  difelcarsg  34301  carsgclctunlem1  34308  carsggect  34309  eulerpartgbij  34363  circlemethhgt  34634  hgt750lemb  34647  bnj1416  35029  f1resfz0f1d  35101  subfacp1lem1  35166  subfacp1lem3  35169  pconnconn  35218  indispconn  35221  satfv1lem  35349  hfun  36166  onint1  36437  bj-fununsn2  37242  pibt2  37405  lindsenlbs  37609  poimirlem3  37617  poimirlem5  37619  poimirlem11  37625  poimirlem12  37626  poimirlem13  37627  poimirlem14  37628  poimirlem15  37629  poimirlem16  37630  poimirlem19  37633  poimirlem20  37634  poimirlem21  37635  poimirlem22  37636  poimirlem28  37642  poimirlem30  37644  padd02  39806  paddcom  39807  pclfinclN  39944  djhcom  41399  elrfi  42682  fzsplit1nn0  42742  eldioph2lem1  42748  eldioph2lem2  42749  diophin  42760  eldioph4b  42799  diophren  42801  kelac2  43054  pwssplit4  43078  iocunico  43200  rp-fakeuninass  43505  iunrelexp0  43691  corcltrcl  43728  frege124d  43750  mnuprdlem1  44261  equncomVD  44857  iunconnlem2  44924  snunioo1  45510  iccdifioo  45513  limciccioolb  45619  sumnnodd  45628  dirkercncflem2  46102  dirkercncflem3  46103  fourierdlem32  46137  fourierdlem93  46197  isomenndlem  46528  hoidmvlelem2  46594  hspmbllem1  46624  hspmbllem2  46625  fsumsplitsndif  47374  isubgr3stgrlem1  47965  usgrexmpl1edg  48015  usgrexmpl2edg  48020  aacllem  49790