Theorem uncom 4112

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

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

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 3444  df-un 3908

This theorem is referenced by:  equncom  4113  uneq2  4116  un12  4127  un23  4128  ssun2  4133  unss2  4141  ssequn2  4143  symdifcom  4208  undir  4241  unineq  4242  dif32  4256  0un  4350  disjpss  4415  undif1  4430  undif2  4431  undifrOLD  4438  difcom  4443  uneqdifeq  4447  dfif4  4497  dfif5  4498  pwundif  4580  prcom  4691  tpass  4711  prprc1  4724  ssunsn2  4785  sspr  4793  sstp  4794  symdifv  5043  iunxdif3  5052  unidif0  5307  difxp2  6132  suc0  6402  fununfun  6548  fnunres2  6613  fresaunres2  6714  fresaunres1  6715  f1oprswap  6827  fvun2  6934  fvsnun2  7139  fsnunfv  7143  fveqf1o  7258  difex2  7715  elpwun  7724  fnsuppeq0  8144  oev2  8460  oacomf1o  8502  undifixp  8884  dfdom2  8927  domunsncan  9017  enfixsn  9026  domunsn  9067  limensuci  9093  findcard2  9101  findcard2s  9102  unfi  9107  ssfi  9109  enp1ilem  9190  frfi  9197  domunfican  9234  fsuppunbi  9304  elfiun  9345  infdifsn  9578  cantnfp1lem3  9601  rankmapu  9802  djuunxp  9845  infunsdom1  10134  infunsdom  10135  infxp  10136  ackbij1lem2  10142  ackbij1lem18  10158  fin1a2lem10  10331  fin1a2lem13  10334  zornn0g  10427  alephadd  10500  fpwwe2lem12  10565  canthp1lem1  10575  xrsupss  13236  xrinfmss  13237  supxrmnf  13244  prunioo  13409  fzsuc2  13510  fzdifsuc  13512  fseq1p1m1  13526  hashinf  14270  hashun3  14319  hashbclem  14387  relexpcnv  14970  fsumsplit1  15680  modfsummods  15728  incexclem  15771  lcmfunsnlem  16580  ramub1lem1  16966  setsid  17146  mreexexlem3d  17581  mreexexlem4d  17582  cnvtsr  18523  symgvalstruct  19338  gsumzaddlem  19862  gsummptfzsplitl  19874  dmdprdsplit2  19989  lspsnat  21112  lsppratlem3  21116  indistopon  22957  indistps  22967  indistps2  22968  ordtcnv  23157  leordtval2  23168  lecldbas  23175  cmpcld  23358  iunconn  23384  ufprim  23865  alexsubALTlem3  24005  ptcmplem1  24008  xpsdsval  24337  iccntr  24778  reconn  24785  volun  25514  voliunlem1  25519  icombl  25533  ioombl  25534  ismbf3d  25623  itgioo  25785  itgsplitioo  25807  lhop  25989  plyeq0  26184  fta1lem  26283  birthdaylem2  26930  lgsquadlem2  27360  nosepdm  27664  addscom  27974  addsproplem4  27980  addsproplem6  27982  negsproplem4  28039  negsproplem6  28041  negbdaylem  28064  mulscom  28147  mulsass  28174  usgrfilem  29412  ex-dif  30510  shjcom  31445  indifundif  32610  imadifxp  32687  difioo  32872  nn0diffz0  32884  gsummulsubdishift1  33161  symgcom  33176  pmtrcnel2  33183  cycpmcl  33209  cycpm2tr  33212  tocyccntz  33237  lindsunlem  33801  lindsun  33802  fldext2rspun  33859  ordtcnvNEW  34097  xrge0iifcnv  34110  prsiga  34308  unelldsys  34335  measun  34388  measunl  34393  difelcarsg  34487  carsgclctunlem1  34494  carsggect  34495  eulerpartgbij  34549  circlemethhgt  34820  hgt750lemb  34833  bnj1416  35214  f1resfz0f1d  35327  subfacp1lem1  35392  subfacp1lem3  35395  pconnconn  35444  indispconn  35447  satfv1lem  35575  hfun  36391  onint1  36662  bj-fununsn2  37506  pibt2  37669  lindsenlbs  37863  poimirlem3  37871  poimirlem5  37873  poimirlem11  37879  poimirlem12  37880  poimirlem13  37881  poimirlem14  37882  poimirlem15  37883  poimirlem16  37884  poimirlem19  37887  poimirlem20  37888  poimirlem21  37889  poimirlem22  37890  poimirlem28  37896  poimirlem30  37898  ecuncnvepres  38643  padd02  40185  paddcom  40186  pclfinclN  40323  djhcom  41778  elrfi  43048  fzsplit1nn0  43108  eldioph2lem1  43114  eldioph2lem2  43115  diophin  43126  eldioph4b  43165  diophren  43167  kelac2  43419  pwssplit4  43443  iocunico  43565  rp-fakeuninass  43869  iunrelexp0  44055  corcltrcl  44092  frege124d  44114  mnuprdlem1  44625  equncomVD  45220  iunconnlem2  45287  snunioo1  45869  iccdifioo  45872  limciccioolb  45978  sumnnodd  45987  dirkercncflem2  46459  dirkercncflem3  46460  fourierdlem32  46494  fourierdlem93  46554  isomenndlem  46885  hoidmvlelem2  46951  hspmbllem1  46981  hspmbllem2  46982  fsumsplitsndif  47730  isubgr3stgrlem1  48323  usgrexmpl1edg  48381  usgrexmpl2edg  48386  aacllem  50157