Theorem uncom 4053

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

Syntax hints:   ∨ wo 847   = wceq 1543   ∈ wcel 2112   ∪ cun 3851

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-tru 1546  df-ex 1788  df-sb 2073  df-clab 2715  df-cleq 2728  df-clel 2809  df-v 3400  df-un 3858

This theorem is referenced by:  equncom  4054  uneq2  4057  un12  4067  un23  4068  ssun2  4073  unss2  4081  ssequn2  4083  symdifcom  4144  undir  4177  unineq  4178  dif32  4193  0un  4293  disjpss  4361  undif1  4376  undif2  4377  difcom  4386  uneqdifeq  4390  dfif4  4440  dfif5  4441  pwundif  4525  prcom  4634  tpass  4654  prprc1  4667  difsnid  4709  ssunsn2  4726  sspr  4732  sstp  4733  symdifv  4980  iunxdif3  4989  unidif0  5236  difxp2  6009  suc0  6265  fununfun  6406  fresaunres2  6569  fresaunres1  6570  f1oprswap  6682  fvun2  6781  fvsnun2  6976  fsnunfv  6980  fveqf1o  7091  f1ofvswap  7094  difex2  7523  elpwun  7532  fnsuppeq0  7912  oev2  8228  oacomf1o  8271  ralxpmap  8555  undifixp  8593  dfdom2  8632  domunsncan  8723  enfixsn  8732  domunsn  8774  limensuci  8800  phplem2  8804  findcard2  8820  findcard2s  8821  unfi  8828  ssfi  8829  enp1ilem  8886  findcard2OLD  8891  frfi  8894  domunfican  8922  fsuppunbi  8984  elfiun  9024  infdifsn  9250  cantnfp1lem3  9273  rankmapu  9459  djuunxp  9502  infunsdom1  9792  infunsdom  9793  infxp  9794  ackbij1lem2  9800  ackbij1lem18  9816  fin1a2lem10  9988  fin1a2lem13  9991  zornn0g  10084  alephadd  10156  fpwwe2lem12  10221  canthp1lem1  10231  xrsupss  12864  xrinfmss  12865  supxrmnf  12872  prunioo  13034  fzsuc2  13135  fzdifsuc  13137  fseq1p1m1  13151  hashinf  13866  hashun3  13916  hashbclem  13981  relexpcnv  14563  modfsummods  15320  incexclem  15363  lcmfunsnlem  16161  ramub1lem1  16542  setsid  16719  mreexexlem3d  17103  mreexexlem4d  17104  cnvtsr  18048  symgvalstruct  18743  gsumzaddlem  19260  gsummptfzsplitl  19272  dmdprdsplit2  19387  lspsnat  20136  lsppratlem3  20140  indistopon  21852  indistps  21862  indistps2  21863  ordtcnv  22052  leordtval2  22063  lecldbas  22070  cmpcld  22253  iunconn  22279  ufprim  22760  alexsubALTlem3  22900  ptcmplem1  22903  xpsdsval  23233  iccntr  23672  reconn  23679  volun  24396  voliunlem1  24401  icombl  24415  ioombl  24416  ismbf3d  24505  itgioo  24667  itgsplitioo  24689  lhop  24867  plyeq0  25059  fta1lem  25154  birthdaylem2  25789  lgsquadlem2  26216  usgrfilem  27369  ex-dif  28460  shjcom  29393  undifr  30545  indifundif  30546  imadifxp  30613  fnunres2  30689  difioo  30777  symgcom  31025  pmtrcnel2  31032  cycpmcl  31056  cycpm2tr  31059  tocyccntz  31084  lindsunlem  31373  lindsun  31374  ordtcnvNEW  31538  xrge0iifcnv  31551  prsiga  31765  unelldsys  31792  measun  31845  measunl  31850  difelcarsg  31943  carsgclctunlem1  31950  carsggect  31951  eulerpartgbij  32005  circlemethhgt  32289  hgt750lemb  32302  bnj1416  32686  f1resfz0f1d  32739  subfacp1lem1  32808  subfacp1lem3  32811  pconnconn  32860  indispconn  32863  satfv1lem  32991  nosepdm  33573  addscom  33815  hfun  34166  onint1  34324  bj-fununsn2  35109  pibt2  35274  lindsenlbs  35458  poimirlem3  35466  poimirlem5  35468  poimirlem11  35474  poimirlem12  35475  poimirlem13  35476  poimirlem14  35477  poimirlem15  35478  poimirlem16  35479  poimirlem19  35482  poimirlem20  35483  poimirlem21  35484  poimirlem22  35485  poimirlem28  35491  poimirlem30  35493  padd02  37512  paddcom  37513  pclfinclN  37650  djhcom  39105  metakunt24  39811  elrfi  40160  fzsplit1nn0  40220  eldioph2lem1  40226  eldioph2lem2  40227  diophin  40238  eldioph4b  40277  diophren  40279  kelac2  40534  pwssplit4  40558  iocunico  40686  rp-fakeuninass  40749  iunrelexp0  40928  corcltrcl  40965  frege124d  40987  mnuprdlem1  41504  equncomVD  42102  iunconnlem2  42169  snunioo1  42666  iccdifioo  42669  fsumsplit1  42731  limciccioolb  42780  sumnnodd  42789  dirkercncflem2  43263  dirkercncflem3  43264  fourierdlem32  43298  fourierdlem93  43358  isomenndlem  43686  hoidmvlelem2  43752  hspmbllem1  43782  hspmbllem2  43783  fsumsplitsndif  44441  aacllem  46119