Theorem uncom 4167

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

Syntax hints:   ∨ wo 847   = wceq 1536   ∈ wcel 2105   ∪ cun 3960

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-v 3479  df-un 3967

This theorem is referenced by:  equncom  4168  uneq2  4171  un12  4182  un23  4183  ssun2  4188  unss2  4196  ssequn2  4198  symdifcom  4259  undir  4292  unineq  4293  dif32  4307  0un  4401  disjpss  4466  undif1  4481  undif2  4482  undifrOLD  4489  difcom  4494  uneqdifeq  4498  dfif4  4545  dfif5  4546  pwundif  4628  prcom  4736  tpass  4756  prprc1  4769  ssunsn2  4831  sspr  4839  sstp  4840  symdifv  5090  iunxdif3  5099  unidif0  5365  difxp2  6187  suc0  6460  fununfun  6615  fnunres2  6681  fresaunres2  6780  fresaunres1  6781  f1oprswap  6892  fvun2  7000  fvsnun2  7202  fsnunfv  7206  fveqf1o  7321  difex2  7778  elpwun  7787  fnsuppeq0  8215  oev2  8559  oacomf1o  8601  undifixp  8972  dfdom2  9016  domunsncan  9110  enfixsn  9119  domunsn  9165  limensuci  9191  findcard2  9202  findcard2s  9203  unfi  9209  ssfi  9211  phplem2OLD  9252  enp1ilem  9309  frfi  9318  domunfican  9358  fsuppunbi  9426  elfiun  9467  infdifsn  9694  cantnfp1lem3  9717  rankmapu  9915  djuunxp  9958  infunsdom1  10249  infunsdom  10250  infxp  10251  ackbij1lem2  10257  ackbij1lem18  10273  fin1a2lem10  10446  fin1a2lem13  10449  zornn0g  10542  alephadd  10614  fpwwe2lem12  10679  canthp1lem1  10689  xrsupss  13347  xrinfmss  13348  supxrmnf  13355  prunioo  13517  fzsuc2  13618  fzdifsuc  13620  fseq1p1m1  13634  hashinf  14370  hashun3  14419  hashbclem  14487  relexpcnv  15070  fsumsplit1  15777  modfsummods  15825  incexclem  15868  lcmfunsnlem  16674  ramub1lem1  17059  setsid  17241  mreexexlem3d  17690  mreexexlem4d  17691  cnvtsr  18645  symgvalstruct  19428  symgvalstructOLD  19429  gsumzaddlem  19953  gsummptfzsplitl  19965  dmdprdsplit2  20080  lspsnat  21164  lsppratlem3  21168  indistopon  23023  indistps  23033  indistps2  23034  ordtcnv  23224  leordtval2  23235  lecldbas  23242  cmpcld  23425  iunconn  23451  ufprim  23932  alexsubALTlem3  24072  ptcmplem1  24075  xpsdsval  24406  iccntr  24856  reconn  24863  volun  25593  voliunlem1  25598  icombl  25612  ioombl  25613  ismbf3d  25702  itgioo  25865  itgsplitioo  25887  lhop  26069  plyeq0  26264  fta1lem  26363  birthdaylem2  27009  lgsquadlem2  27439  nosepdm  27743  addscom  28013  addsproplem4  28019  addsproplem6  28021  negsproplem4  28077  negsproplem6  28079  negsbdaylem  28102  mulscom  28179  mulsass  28206  usgrfilem  29358  ex-dif  30451  shjcom  31386  indifundif  32551  imadifxp  32620  difioo  32790  symgcom  33085  pmtrcnel2  33092  cycpmcl  33118  cycpm2tr  33121  tocyccntz  33146  lindsunlem  33651  lindsun  33652  ordtcnvNEW  33880  xrge0iifcnv  33893  prsiga  34111  unelldsys  34138  measun  34191  measunl  34196  difelcarsg  34291  carsgclctunlem1  34298  carsggect  34299  eulerpartgbij  34353  circlemethhgt  34636  hgt750lemb  34649  bnj1416  35031  f1resfz0f1d  35097  subfacp1lem1  35163  subfacp1lem3  35166  pconnconn  35215  indispconn  35218  satfv1lem  35346  hfun  36159  onint1  36431  bj-fununsn2  37236  pibt2  37399  lindsenlbs  37601  poimirlem3  37609  poimirlem5  37611  poimirlem11  37617  poimirlem12  37618  poimirlem13  37619  poimirlem14  37620  poimirlem15  37621  poimirlem16  37622  poimirlem19  37625  poimirlem20  37626  poimirlem21  37627  poimirlem22  37628  poimirlem28  37634  poimirlem30  37636  padd02  39794  paddcom  39795  pclfinclN  39932  djhcom  41387  metakunt24  42209  elrfi  42681  fzsplit1nn0  42741  eldioph2lem1  42747  eldioph2lem2  42748  diophin  42759  eldioph4b  42798  diophren  42800  kelac2  43053  pwssplit4  43077  iocunico  43199  rp-fakeuninass  43505  iunrelexp0  43691  corcltrcl  43728  frege124d  43750  mnuprdlem1  44267  equncomVD  44865  iunconnlem2  44932  snunioo1  45464  iccdifioo  45467  limciccioolb  45576  sumnnodd  45585  dirkercncflem2  46059  dirkercncflem3  46060  fourierdlem32  46094  fourierdlem93  46154  isomenndlem  46485  hoidmvlelem2  46551  hspmbllem1  46581  hspmbllem2  46582  fsumsplitsndif  47297  isubgr3stgrlem1  47868  usgrexmpl1edg  47918  usgrexmpl2edg  47923  aacllem  49031