Theorem uncom 4158

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

Syntax hints:   ∨ wo 848   = wceq 1540   ∈ wcel 2108   ∪ cun 3949

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-un 3956

This theorem is referenced by:  equncom  4159  uneq2  4162  un12  4173  un23  4174  ssun2  4179  unss2  4187  ssequn2  4189  symdifcom  4254  undir  4287  unineq  4288  dif32  4302  0un  4396  disjpss  4461  undif1  4476  undif2  4477  undifrOLD  4484  difcom  4489  uneqdifeq  4493  dfif4  4541  dfif5  4542  pwundif  4624  prcom  4732  tpass  4752  prprc1  4765  ssunsn2  4827  sspr  4835  sstp  4836  symdifv  5086  iunxdif3  5095  unidif0  5360  difxp2  6186  suc0  6459  fununfun  6614  fnunres2  6681  fresaunres2  6780  fresaunres1  6781  f1oprswap  6892  fvun2  7001  fvsnun2  7203  fsnunfv  7207  fveqf1o  7322  difex2  7780  elpwun  7789  fnsuppeq0  8217  oev2  8561  oacomf1o  8603  undifixp  8974  dfdom2  9018  domunsncan  9112  enfixsn  9121  domunsn  9167  limensuci  9193  findcard2  9204  findcard2s  9205  unfi  9211  ssfi  9213  phplem2OLD  9255  enp1ilem  9312  frfi  9321  domunfican  9361  fsuppunbi  9429  elfiun  9470  infdifsn  9697  cantnfp1lem3  9720  rankmapu  9918  djuunxp  9961  infunsdom1  10252  infunsdom  10253  infxp  10254  ackbij1lem2  10260  ackbij1lem18  10276  fin1a2lem10  10449  fin1a2lem13  10452  zornn0g  10545  alephadd  10617  fpwwe2lem12  10682  canthp1lem1  10692  xrsupss  13351  xrinfmss  13352  supxrmnf  13359  prunioo  13521  fzsuc2  13622  fzdifsuc  13624  fseq1p1m1  13638  hashinf  14374  hashun3  14423  hashbclem  14491  relexpcnv  15074  fsumsplit1  15781  modfsummods  15829  incexclem  15872  lcmfunsnlem  16678  ramub1lem1  17064  setsid  17244  mreexexlem3d  17689  mreexexlem4d  17690  cnvtsr  18633  symgvalstruct  19414  symgvalstructOLD  19415  gsumzaddlem  19939  gsummptfzsplitl  19951  dmdprdsplit2  20066  lspsnat  21147  lsppratlem3  21151  indistopon  23008  indistps  23018  indistps2  23019  ordtcnv  23209  leordtval2  23220  lecldbas  23227  cmpcld  23410  iunconn  23436  ufprim  23917  alexsubALTlem3  24057  ptcmplem1  24060  xpsdsval  24391  iccntr  24843  reconn  24850  volun  25580  voliunlem1  25585  icombl  25599  ioombl  25600  ismbf3d  25689  itgioo  25851  itgsplitioo  25873  lhop  26055  plyeq0  26250  fta1lem  26349  birthdaylem2  26995  lgsquadlem2  27425  nosepdm  27729  addscom  27999  addsproplem4  28005  addsproplem6  28007  negsproplem4  28063  negsproplem6  28065  negsbdaylem  28088  mulscom  28165  mulsass  28192  usgrfilem  29344  ex-dif  30442  shjcom  31377  indifundif  32543  imadifxp  32614  difioo  32784  symgcom  33103  pmtrcnel2  33110  cycpmcl  33136  cycpm2tr  33139  tocyccntz  33164  lindsunlem  33675  lindsun  33676  fldext2rspun  33732  ordtcnvNEW  33919  xrge0iifcnv  33932  prsiga  34132  unelldsys  34159  measun  34212  measunl  34217  difelcarsg  34312  carsgclctunlem1  34319  carsggect  34320  eulerpartgbij  34374  circlemethhgt  34658  hgt750lemb  34671  bnj1416  35053  f1resfz0f1d  35119  subfacp1lem1  35184  subfacp1lem3  35187  pconnconn  35236  indispconn  35239  satfv1lem  35367  hfun  36179  onint1  36450  bj-fununsn2  37255  pibt2  37418  lindsenlbs  37622  poimirlem3  37630  poimirlem5  37632  poimirlem11  37638  poimirlem12  37639  poimirlem13  37640  poimirlem14  37641  poimirlem15  37642  poimirlem16  37643  poimirlem19  37646  poimirlem20  37647  poimirlem21  37648  poimirlem22  37649  poimirlem28  37655  poimirlem30  37657  padd02  39814  paddcom  39815  pclfinclN  39952  djhcom  41407  metakunt24  42229  elrfi  42705  fzsplit1nn0  42765  eldioph2lem1  42771  eldioph2lem2  42772  diophin  42783  eldioph4b  42822  diophren  42824  kelac2  43077  pwssplit4  43101  iocunico  43223  rp-fakeuninass  43529  iunrelexp0  43715  corcltrcl  43752  frege124d  43774  mnuprdlem1  44291  equncomVD  44888  iunconnlem2  44955  snunioo1  45525  iccdifioo  45528  limciccioolb  45636  sumnnodd  45645  dirkercncflem2  46119  dirkercncflem3  46120  fourierdlem32  46154  fourierdlem93  46214  isomenndlem  46545  hoidmvlelem2  46611  hspmbllem1  46641  hspmbllem2  46642  fsumsplitsndif  47360  isubgr3stgrlem1  47933  usgrexmpl1edg  47983  usgrexmpl2edg  47988  aacllem  49320