Theorem uncom 4107

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

Syntax hints:   ∨ wo 847   = wceq 1541   ∈ wcel 2113   ∪ cun 3896

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-v 3439  df-un 3903

This theorem is referenced by:  equncom  4108  uneq2  4111  un12  4122  un23  4123  ssun2  4128  unss2  4136  ssequn2  4138  symdifcom  4203  undir  4236  unineq  4237  dif32  4251  0un  4345  disjpss  4410  undif1  4425  undif2  4426  undifrOLD  4433  difcom  4438  uneqdifeq  4442  dfif4  4492  dfif5  4493  pwundif  4575  prcom  4686  tpass  4706  prprc1  4719  ssunsn2  4780  sspr  4788  sstp  4789  symdifv  5038  iunxdif3  5047  unidif0  5302  difxp2  6120  suc0  6390  fununfun  6536  fnunres2  6601  fresaunres2  6702  fresaunres1  6703  f1oprswap  6815  fvun2  6922  fvsnun2  7125  fsnunfv  7129  fveqf1o  7244  difex2  7701  elpwun  7710  fnsuppeq0  8130  oev2  8446  oacomf1o  8488  undifixp  8866  dfdom2  8909  domunsncan  8999  enfixsn  9008  domunsn  9049  limensuci  9075  findcard2  9083  findcard2s  9084  unfi  9089  ssfi  9091  enp1ilem  9171  frfi  9178  domunfican  9215  fsuppunbi  9282  elfiun  9323  infdifsn  9556  cantnfp1lem3  9579  rankmapu  9780  djuunxp  9823  infunsdom1  10112  infunsdom  10113  infxp  10114  ackbij1lem2  10120  ackbij1lem18  10136  fin1a2lem10  10309  fin1a2lem13  10312  zornn0g  10405  alephadd  10477  fpwwe2lem12  10542  canthp1lem1  10552  xrsupss  13212  xrinfmss  13213  supxrmnf  13220  prunioo  13385  fzsuc2  13486  fzdifsuc  13488  fseq1p1m1  13502  hashinf  14246  hashun3  14295  hashbclem  14363  relexpcnv  14946  fsumsplit1  15656  modfsummods  15704  incexclem  15747  lcmfunsnlem  16556  ramub1lem1  16942  setsid  17122  mreexexlem3d  17556  mreexexlem4d  17557  cnvtsr  18498  symgvalstruct  19313  gsumzaddlem  19837  gsummptfzsplitl  19849  dmdprdsplit2  19964  lspsnat  21086  lsppratlem3  21090  indistopon  22919  indistps  22929  indistps2  22930  ordtcnv  23119  leordtval2  23130  lecldbas  23137  cmpcld  23320  iunconn  23346  ufprim  23827  alexsubALTlem3  23967  ptcmplem1  23970  xpsdsval  24299  iccntr  24740  reconn  24747  volun  25476  voliunlem1  25481  icombl  25495  ioombl  25496  ismbf3d  25585  itgioo  25747  itgsplitioo  25769  lhop  25951  plyeq0  26146  fta1lem  26245  birthdaylem2  26892  lgsquadlem2  27322  nosepdm  27626  addscom  27912  addsproplem4  27918  addsproplem6  27920  negsproplem4  27976  negsproplem6  27978  negsbdaylem  28001  mulscom  28081  mulsass  28108  usgrfilem  29309  ex-dif  30407  shjcom  31342  indifundif  32508  imadifxp  32585  difioo  32771  nn0diffz0  32783  symgcom  33061  pmtrcnel2  33068  cycpmcl  33094  cycpm2tr  33097  tocyccntz  33122  lindsunlem  33660  lindsun  33661  fldext2rspun  33718  ordtcnvNEW  33956  xrge0iifcnv  33969  prsiga  34167  unelldsys  34194  measun  34247  measunl  34252  difelcarsg  34346  carsgclctunlem1  34353  carsggect  34354  eulerpartgbij  34408  circlemethhgt  34679  hgt750lemb  34692  bnj1416  35074  f1resfz0f1d  35181  subfacp1lem1  35246  subfacp1lem3  35249  pconnconn  35298  indispconn  35301  satfv1lem  35429  hfun  36245  onint1  36516  bj-fununsn2  37321  pibt2  37484  lindsenlbs  37678  poimirlem3  37686  poimirlem5  37688  poimirlem11  37694  poimirlem12  37695  poimirlem13  37696  poimirlem14  37697  poimirlem15  37698  poimirlem16  37699  poimirlem19  37702  poimirlem20  37703  poimirlem21  37704  poimirlem22  37705  poimirlem28  37711  poimirlem30  37713  ecuncnvepres  38442  padd02  39934  paddcom  39935  pclfinclN  40072  djhcom  41527  elrfi  42814  fzsplit1nn0  42874  eldioph2lem1  42880  eldioph2lem2  42881  diophin  42892  eldioph4b  42931  diophren  42933  kelac2  43185  pwssplit4  43209  iocunico  43331  rp-fakeuninass  43636  iunrelexp0  43822  corcltrcl  43859  frege124d  43881  mnuprdlem1  44392  equncomVD  44987  iunconnlem2  45054  snunioo1  45639  iccdifioo  45642  limciccioolb  45748  sumnnodd  45757  dirkercncflem2  46229  dirkercncflem3  46230  fourierdlem32  46264  fourierdlem93  46324  isomenndlem  46655  hoidmvlelem2  46721  hspmbllem1  46751  hspmbllem2  46752  fsumsplitsndif  47500  isubgr3stgrlem1  48093  usgrexmpl1edg  48151  usgrexmpl2edg  48156  aacllem  49929