Theorem uncom 4087

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 867	. . 3 ⊢ ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) ↔ (𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐴))
2		elun 4083	. . 3 ⊢ (𝑥 ∈ (𝐵 ∪ 𝐴) ↔ (𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐴))
3	1, 2	bitr4i 277	. 2 ⊢ ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ (𝐵 ∪ 𝐴))
4	3	uneqri 4085	1 ⊢ (𝐴 ∪ 𝐵) = (𝐵 ∪ 𝐴)

Syntax hints:   ∨ wo 844   = wceq 1539   ∈ wcel 2106   ∪ cun 3885

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3434  df-un 3892

This theorem is referenced by:  equncom  4088  uneq2  4091  un12  4101  un23  4102  ssun2  4107  unss2  4115  ssequn2  4117  symdifcom  4177  undir  4210  unineq  4211  dif32  4226  0un  4326  disjpss  4394  undif1  4409  undif2  4410  difcom  4419  uneqdifeq  4423  dfif4  4474  dfif5  4475  pwundif  4559  prcom  4668  tpass  4688  prprc1  4701  difsnid  4743  ssunsn2  4760  sspr  4766  sstp  4767  symdifv  5015  iunxdif3  5024  unidif0  5282  difxp2  6069  suc0  6340  fununfun  6482  fresaunres2  6646  fresaunres1  6647  f1oprswap  6760  fvun2  6860  fvsnun2  7055  fsnunfv  7059  fveqf1o  7175  f1ofvswap  7178  difex2  7610  elpwun  7619  fnsuppeq0  8008  oev2  8353  oacomf1o  8396  ralxpmap  8684  undifixp  8722  dfdom2  8766  domunsncan  8859  enfixsn  8868  domunsn  8914  limensuci  8940  findcard2  8947  findcard2s  8948  unfi  8955  ssfi  8956  phplem2OLD  9001  enp1ilem  9051  findcard2OLD  9056  frfi  9059  domunfican  9087  fsuppunbi  9149  elfiun  9189  infdifsn  9415  cantnfp1lem3  9438  rankmapu  9636  djuunxp  9679  infunsdom1  9969  infunsdom  9970  infxp  9971  ackbij1lem2  9977  ackbij1lem18  9993  fin1a2lem10  10165  fin1a2lem13  10168  zornn0g  10261  alephadd  10333  fpwwe2lem12  10398  canthp1lem1  10408  xrsupss  13043  xrinfmss  13044  supxrmnf  13051  prunioo  13213  fzsuc2  13314  fzdifsuc  13316  fseq1p1m1  13330  hashinf  14049  hashun3  14099  hashbclem  14164  relexpcnv  14746  fsumsplit1  15457  modfsummods  15505  incexclem  15548  lcmfunsnlem  16346  ramub1lem1  16727  setsid  16909  mreexexlem3d  17355  mreexexlem4d  17356  cnvtsr  18306  symgvalstruct  19004  symgvalstructOLD  19005  gsumzaddlem  19522  gsummptfzsplitl  19534  dmdprdsplit2  19649  lspsnat  20407  lsppratlem3  20411  indistopon  22151  indistps  22161  indistps2  22162  ordtcnv  22352  leordtval2  22363  lecldbas  22370  cmpcld  22553  iunconn  22579  ufprim  23060  alexsubALTlem3  23200  ptcmplem1  23203  xpsdsval  23534  iccntr  23984  reconn  23991  volun  24709  voliunlem1  24714  icombl  24728  ioombl  24729  ismbf3d  24818  itgioo  24980  itgsplitioo  25002  lhop  25180  plyeq0  25372  fta1lem  25467  birthdaylem2  26102  lgsquadlem2  26529  usgrfilem  27694  ex-dif  28787  shjcom  29720  undifr  30872  indifundif  30873  imadifxp  30940  fnunres2  31015  difioo  31103  symgcom  31352  pmtrcnel2  31359  cycpmcl  31383  cycpm2tr  31386  tocyccntz  31411  lindsunlem  31705  lindsun  31706  ordtcnvNEW  31870  xrge0iifcnv  31883  prsiga  32099  unelldsys  32126  measun  32179  measunl  32184  difelcarsg  32277  carsgclctunlem1  32284  carsggect  32285  eulerpartgbij  32339  circlemethhgt  32623  hgt750lemb  32636  bnj1416  33019  f1resfz0f1d  33072  subfacp1lem1  33141  subfacp1lem3  33144  pconnconn  33193  indispconn  33196  satfv1lem  33324  nosepdm  33887  addscom  34129  hfun  34480  onint1  34638  bj-fununsn2  35425  pibt2  35588  lindsenlbs  35772  poimirlem3  35780  poimirlem5  35782  poimirlem11  35788  poimirlem12  35789  poimirlem13  35790  poimirlem14  35791  poimirlem15  35792  poimirlem16  35793  poimirlem19  35796  poimirlem20  35797  poimirlem21  35798  poimirlem22  35799  poimirlem28  35805  poimirlem30  35807  padd02  37826  paddcom  37827  pclfinclN  37964  djhcom  39419  metakunt24  40148  elrfi  40516  fzsplit1nn0  40576  eldioph2lem1  40582  eldioph2lem2  40583  diophin  40594  eldioph4b  40633  diophren  40635  kelac2  40890  pwssplit4  40914  iocunico  41042  rp-fakeuninass  41123  iunrelexp0  41310  corcltrcl  41347  frege124d  41369  mnuprdlem1  41890  equncomVD  42488  iunconnlem2  42555  snunioo1  43050  iccdifioo  43053  limciccioolb  43162  sumnnodd  43171  dirkercncflem2  43645  dirkercncflem3  43646  fourierdlem32  43680  fourierdlem93  43740  isomenndlem  44068  hoidmvlelem2  44134  hspmbllem1  44164  hspmbllem2  44165  fsumsplitsndif  44825  aacllem  46505