Theorem uncom 4128

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 866	. . 3 ⊢ ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) ↔ (𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐴))
2		elun 4124	. . 3 ⊢ (𝑥 ∈ (𝐵 ∪ 𝐴) ↔ (𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐴))
3	1, 2	bitr4i 280	. 2 ⊢ ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ (𝐵 ∪ 𝐴))
4	3	uneqri 4126	1 ⊢ (𝐴 ∪ 𝐵) = (𝐵 ∪ 𝐴)

Syntax hints:   ∨ wo 843   = wceq 1533   ∈ wcel 2110   ∪ cun 3933

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-v 3496  df-un 3940

This theorem is referenced by:  equncom  4129  uneq2  4132  un12  4142  un23  4143  ssun2  4148  unss2  4156  ssequn2  4158  symdifcom  4219  undir  4252  unineq  4253  dif32  4266  0un  4345  disjpss  4409  undif1  4423  undif2  4424  difcom  4433  uneqdifeq  4437  dfif4  4481  dfif5  4482  pwundif  4564  prcom  4667  tpass  4687  prprc1  4700  difsnid  4742  ssunsn2  4759  sspr  4765  sstp  4766  symdifv  5007  iunxdif3  5016  unidif0  5259  difxp2  6022  suc0  6264  fununfun  6401  fresaunres2  6549  fresaunres1  6550  f1oprswap  6657  fvun2  6754  fvsnun2  6944  fsnunfv  6948  fveqf1o  7057  difex2  7481  elpwun  7490  fnsuppeq0  7857  oev2  8147  oacomf1o  8190  ralxpmap  8459  undifixp  8497  dfdom2  8534  domunsncan  8616  enfixsn  8625  domunsn  8666  limensuci  8692  phplem2  8696  enp1ilem  8751  findcard2  8757  findcard2s  8758  frfi  8762  domunfican  8790  fsuppunbi  8853  elfiun  8893  infdifsn  9119  cantnfp1lem3  9142  rankmapu  9306  djuunxp  9349  infunsdom1  9634  infunsdom  9635  infxp  9636  ackbij1lem2  9642  ackbij1lem18  9658  fin1a2lem10  9830  fin1a2lem13  9833  zornn0g  9926  alephadd  9998  fpwwe2lem13  10063  canthp1lem1  10073  xrsupss  12701  xrinfmss  12702  supxrmnf  12709  prunioo  12866  fzsuc2  12964  fzdifsuc  12966  fseq1p1m1  12980  hashinf  13694  hashun3  13744  hashbclem  13809  relexpcnv  14393  modfsummods  15147  incexclem  15190  lcmfunsnlem  15984  ramub1lem1  16361  setsid  16537  mreexexlem3d  16916  mreexexlem4d  16917  cnvtsr  17831  symgvalstruct  18524  gsumzaddlem  19040  gsummptfzsplitl  19052  dmdprdsplit2  19167  lspsnat  19916  lsppratlem3  19920  indistopon  21608  indistps  21618  indistps2  21619  ordtcnv  21808  leordtval2  21819  lecldbas  21826  cmpcld  22009  iunconn  22035  ufprim  22516  alexsubALTlem3  22656  ptcmplem1  22659  xpsdsval  22990  iccntr  23428  reconn  23435  volun  24145  voliunlem1  24150  icombl  24164  ioombl  24165  ismbf3d  24254  itgioo  24415  itgsplitioo  24437  lhop  24612  plyeq0  24800  fta1lem  24895  birthdaylem2  25529  lgsquadlem2  25956  usgrfilem  27108  ex-dif  28201  shjcom  29134  undifr  30283  indifundif  30284  imadifxp  30350  fnunres2  30423  difioo  30504  symgcom  30727  pmtrcnel2  30734  cycpmcl  30758  cycpm2tr  30761  tocyccntz  30786  lindsunlem  31020  lindsun  31021  ordtcnvNEW  31163  xrge0iifcnv  31176  prsiga  31390  unelldsys  31417  measun  31470  measunl  31475  difelcarsg  31568  carsgclctunlem1  31575  carsggect  31576  eulerpartgbij  31630  circlemethhgt  31914  hgt750lemb  31927  bnj1416  32311  f1resfz0f1d  32361  subfacp1lem1  32426  subfacp1lem3  32429  pconnconn  32478  indispconn  32481  satfv1lem  32609  nosepdm  33188  hfun  33639  onint1  33797  bj-fununsn2  34535  pibt2  34697  lindsenlbs  34886  poimirlem3  34894  poimirlem5  34896  poimirlem11  34902  poimirlem12  34903  poimirlem13  34904  poimirlem14  34905  poimirlem15  34906  poimirlem16  34907  poimirlem19  34910  poimirlem20  34911  poimirlem21  34912  poimirlem22  34913  poimirlem28  34919  poimirlem30  34921  padd02  36947  paddcom  36948  pclfinclN  37085  djhcom  38540  elrfi  39289  fzsplit1nn0  39349  eldioph2lem1  39355  eldioph2lem2  39356  diophin  39367  eldioph4b  39406  diophren  39408  kelac2  39663  pwssplit4  39687  iocunico  39815  rp-fakeuninass  39880  iunrelexp0  40045  corcltrcl  40082  frege124d  40104  mnuprdlem1  40606  equncomVD  41200  iunconnlem2  41267  snunioo1  41786  iccdifioo  41789  fsumsplit1  41851  limciccioolb  41900  sumnnodd  41909  dirkercncflem2  42388  dirkercncflem3  42389  fourierdlem32  42423  fourierdlem93  42483  isomenndlem  42811  hoidmvlelem2  42877  hspmbllem1  42907  hspmbllem2  42908  fsumsplitsndif  43532  aacllem  44901