Theorem uncom 4108

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

This proof depends on syntax axioms:   ∨ wo 861   = wceq 1570   ∈ wcel 2145   ∪ cun 3900

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3455  df-un 3907

This theorem is used by:  equncom  4109  uneq2  4112  un12  4122  un23  4123  ssun2  4128  unss2  4136  ssequn2  4138  symdifcom  4203  undir  4236  unineq  4237  dif32  4251  0un  4349  disjpss  4417  undif1  4433  undif2  4434  difcom  4447  uneqdifeq  4451  dfif4  4501  dfif5  4502  pwundif  4585  prcom  4696  tpass  4716  prprc1  4729  ssunsn2  4791  sstp  4799  unidif0OLD  5329  difxp2  6162  suc0  6439  fununfun  6585  fnunres2  6649  fresaunres2  6751  fresaunres1  6752  f1oprswap  6867  fvun2  6974  fvsnun2  7185  fsnunfv  7189  fveqf1o  7307  difex2  7763  elpwun  7772  fnsuppeq0  8194  oev2  8514  oacomf1o  8556  undifixp  8945  dfdom2  8988  domunsncan  9079  enfixsn  9088  domunsn  9129  limensuci  9155  findcard2  9163  findcard2s  9164  unfi  9169  ssfi  9171  enp1ilem  9252  frfi  9259  domunfican  9295  fsuppunbi  9363  elfiun  9404  infdifsn  9640  cantnfp1lem3  9663  rankmapu  9864  djuunxp  9930  infunsdom1  10218  infunsdom  10219  infxp  10220  ackbij1lem2  10226  ackbij1lem18  10242  fin1a2lem10  10415  fin1a2lem13  10418  zornn0g  10511  alephadd  10590  fpwwe2lem12  10655  canthp1lem1  10665  xrsupss  13365  xrinfmss  13366  supxrmnf  13373  prunioo  13538  fzsuc2  13641  fzdifsuc  13643  fseq1p1m1  13657  f1resfz0f1d  13852  hashinf  14403  hashun3  14452  hashbclem  14521  relexpcnv  15112  fsumsplit1  15835  modfsummods  15884  incexclem  15929  lcmfunsnlem  16737  ramub1lem1  17124  setsid  17305  mreexexlem3d  17740  mreexexlem4d  17741  cnvtsr  18682  symgvalstruct  19530  gsumzaddlem  20054  gsummptfzsplitl  20066  dmdprdsplit2  20181  lspsnat  21338  lsppratlem3  21342  lindsenlbs  22070  indistopon  23232  indistps  23242  indistps2  23243  ordtcnv  23432  leordtval2  23443  lecldbas  23450  cmpcld  23633  iunconn  23659  ufprim  24141  alexsubALTlem3  24281  ptcmplem1  24284  xpsdsval  24613  iccntr  25054  reconn  25061  volun  25779  voliunlem1  25784  icombl  25798  ioombl  25799  ismbf3d  25888  itgioo  26050  itgsplitioo  26072  lhop  26250  plyeq0  26444  fta1lem  26544  birthdaylem2  27197  lgsquadlem2  27625  nosepdm  27928  addscom  28239  addsproplem4  28245  addsproplem6  28247  negsproplem4  28304  negsproplem6  28306  negbdaylem  28329  mulscom  28412  mulsass  28439  usgrfilem  29795  ex-dif  30911  shjcom  31847  indifundif  33007  imadifxp  33082  difioo  33261  nn0diffz0  33273  gsummulsubdishift1  33516  symgcom  33531  pmtrcnel2  33538  cycpmcl  33564  cycpm2tr  33567  tocyccntz  33592  lindsunlem  34142  lindsun  34143  fldext2rspun  34200  ordtcnvNEW  34438  xrge0iifcnv  34451  prsiga  34649  unelldsys  34677  measun  34730  measunl  34735  difelcarsg  34829  carsgclctunlem1  34836  carsggect  34837  eulerpartgbij  34891  circlemethhgt  35159  hgt750lemb  35172  bnj1416  35556  subfacp1lem1  35766  subfacp1lem3  35769  pconnconn  35818  indispconn  35821  satfv1lem  35949  hfun  36766  onint1  37076  bj-fununsn2  38014  pibt2  38179  poimirlem3  38380  poimirlem5  38382  poimirlem11  38388  poimirlem12  38389  poimirlem13  38390  poimirlem14  38391  poimirlem15  38392  poimirlem16  38393  poimirlem19  38396  poimirlem20  38397  poimirlem21  38398  poimirlem22  38399  poimirlem28  38405  poimirlem30  38407  ecuncnvepres  39151  padd02  40693  paddcom  40694  pclfinclN  40831  djhcom  42286  elrfi  43547  fzsplit1nn0  43607  eldioph2lem1  43613  eldioph2lem2  43614  diophin  43625  eldioph4b  43660  diophren  43662  kelac2  43914  pwssplit4  43938  iocunico  44060  rp-fakeuninass  44364  iunrelexp0  44550  corcltrcl  44587  frege124d  44609  mnuprdlem1  45104  equncomVD  45698  iunconnlem2  45765  snunioo1  46350  iccdifioo  46353  limciccioolb  46459  sumnnodd  46468  dirkercncflem2  46940  dirkercncflem3  46941  fourierdlem32  46975  fourierdlem93  47035  isomenndlem  47366  hoidmvlelem2  47432  hspmbllem1  47462  hspmbllem2  47463  fsumsplitsndif  48277  isubgr3stgrlem1  48890  usgrexmpl1edg  48948  usgrexmpl2edg  48953  aacllem  50780