Theorem uncom 4181

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

Syntax hints:   ∨ wo 846   = wceq 1537   ∈ wcel 2108   ∪ cun 3974

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-un 3981

This theorem is referenced by:  equncom  4182  uneq2  4185  un12  4196  un23  4197  ssun2  4202  unss2  4210  ssequn2  4212  symdifcom  4273  undir  4306  unineq  4307  dif32  4321  0un  4419  disjpss  4484  undif1  4499  undif2  4500  undifrOLD  4507  difcom  4512  uneqdifeq  4516  dfif4  4563  dfif5  4564  pwundif  4646  prcom  4757  tpass  4777  prprc1  4790  ssunsn2  4852  sspr  4860  sstp  4861  symdifv  5109  iunxdif3  5118  unidif0  5378  difxp2  6197  suc0  6470  fununfun  6626  fnunres2  6692  fresaunres2  6793  fresaunres1  6794  f1oprswap  6906  fvun2  7014  fvsnun2  7217  fsnunfv  7221  fveqf1o  7338  difex2  7795  elpwun  7804  fnsuppeq0  8233  oev2  8579  oacomf1o  8621  undifixp  8992  dfdom2  9038  domunsncan  9138  enfixsn  9147  domunsn  9193  limensuci  9219  findcard2  9230  findcard2s  9231  unfi  9238  ssfi  9240  phplem2OLD  9281  enp1ilem  9340  frfi  9349  domunfican  9389  fsuppunbi  9458  elfiun  9499  infdifsn  9726  cantnfp1lem3  9749  rankmapu  9947  djuunxp  9990  infunsdom1  10281  infunsdom  10282  infxp  10283  ackbij1lem2  10289  ackbij1lem18  10305  fin1a2lem10  10478  fin1a2lem13  10481  zornn0g  10574  alephadd  10646  fpwwe2lem12  10711  canthp1lem1  10721  xrsupss  13371  xrinfmss  13372  supxrmnf  13379  prunioo  13541  fzsuc2  13642  fzdifsuc  13644  fseq1p1m1  13658  hashinf  14384  hashun3  14433  hashbclem  14501  relexpcnv  15084  fsumsplit1  15793  modfsummods  15841  incexclem  15884  lcmfunsnlem  16688  ramub1lem1  17073  setsid  17255  mreexexlem3d  17704  mreexexlem4d  17705  cnvtsr  18658  symgvalstruct  19438  symgvalstructOLD  19439  gsumzaddlem  19963  gsummptfzsplitl  19975  dmdprdsplit2  20090  lspsnat  21170  lsppratlem3  21174  indistopon  23029  indistps  23039  indistps2  23040  ordtcnv  23230  leordtval2  23241  lecldbas  23248  cmpcld  23431  iunconn  23457  ufprim  23938  alexsubALTlem3  24078  ptcmplem1  24081  xpsdsval  24412  iccntr  24862  reconn  24869  volun  25599  voliunlem1  25604  icombl  25618  ioombl  25619  ismbf3d  25708  itgioo  25871  itgsplitioo  25893  lhop  26075  plyeq0  26270  fta1lem  26367  birthdaylem2  27013  lgsquadlem2  27443  nosepdm  27747  addscom  28017  addsproplem4  28023  addsproplem6  28025  negsproplem4  28081  negsproplem6  28083  negsbdaylem  28106  mulscom  28183  mulsass  28210  usgrfilem  29362  ex-dif  30455  shjcom  31390  indifundif  32554  imadifxp  32623  difioo  32787  symgcom  33076  pmtrcnel2  33083  cycpmcl  33109  cycpm2tr  33112  tocyccntz  33137  lindsunlem  33637  lindsun  33638  ordtcnvNEW  33866  xrge0iifcnv  33879  prsiga  34095  unelldsys  34122  measun  34175  measunl  34180  difelcarsg  34275  carsgclctunlem1  34282  carsggect  34283  eulerpartgbij  34337  circlemethhgt  34620  hgt750lemb  34633  bnj1416  35015  f1resfz0f1d  35081  subfacp1lem1  35147  subfacp1lem3  35150  pconnconn  35199  indispconn  35202  satfv1lem  35330  hfun  36142  onint1  36415  bj-fununsn2  37220  pibt2  37383  lindsenlbs  37575  poimirlem3  37583  poimirlem5  37585  poimirlem11  37591  poimirlem12  37592  poimirlem13  37593  poimirlem14  37594  poimirlem15  37595  poimirlem16  37596  poimirlem19  37599  poimirlem20  37600  poimirlem21  37601  poimirlem22  37602  poimirlem28  37608  poimirlem30  37610  padd02  39769  paddcom  39770  pclfinclN  39907  djhcom  41362  metakunt24  42185  elrfi  42650  fzsplit1nn0  42710  eldioph2lem1  42716  eldioph2lem2  42717  diophin  42728  eldioph4b  42767  diophren  42769  kelac2  43022  pwssplit4  43046  iocunico  43172  rp-fakeuninass  43478  iunrelexp0  43664  corcltrcl  43701  frege124d  43723  mnuprdlem1  44241  equncomVD  44839  iunconnlem2  44906  snunioo1  45430  iccdifioo  45433  limciccioolb  45542  sumnnodd  45551  dirkercncflem2  46025  dirkercncflem3  46026  fourierdlem32  46060  fourierdlem93  46120  isomenndlem  46451  hoidmvlelem2  46517  hspmbllem1  46547  hspmbllem2  46548  fsumsplitsndif  47247  usgrexmpl1edg  47839  usgrexmpl2edg  47844  aacllem  48895