Theorem uncom 4115

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

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

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 2148  ax-9 2156  ax-ext 2738

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 2745  df-cleq 2758  df-clel 2841  df-v 3460  df-un 3913

This theorem is used by:  equncom  4116  uneq2  4119  un12  4129  un23  4130  ssun2  4135  unss2  4143  ssequn2  4145  symdifcom  4210  undir  4243  unineq  4244  dif32  4258  0un  4356  disjpss  4424  undif1  4440  undif2  4441  difcom  4454  uneqdifeq  4458  dfif4  4508  dfif5  4509  pwundif  4592  prcom  4703  tpass  4723  prprc1  4736  ssunsn2  4798  sstp  4806  unidif0OLD  5336  difxp2  6168  suc0  6445  fununfun  6591  fnunres2  6655  fresaunres2  6757  fresaunres1  6758  f1oprswap  6873  fvun2  6980  fvsnun2  7188  fsnunfv  7192  fveqf1o  7311  difex2  7768  elpwun  7777  fnsuppeq0  8197  oev2  8517  oacomf1o  8559  undifixp  8941  dfdom2  8984  domunsncan  9075  enfixsn  9084  domunsn  9125  limensuci  9151  findcard2  9159  findcard2s  9160  unfi  9165  ssfi  9167  enp1ilem  9248  frfi  9255  domunfican  9291  fsuppunbi  9359  elfiun  9400  infdifsn  9636  cantnfp1lem3  9659  rankmapu  9860  djuunxp  9926  infunsdom1  10214  infunsdom  10215  infxp  10216  ackbij1lem2  10222  ackbij1lem18  10238  fin1a2lem10  10411  fin1a2lem13  10414  zornn0g  10507  alephadd  10580  fpwwe2lem12  10645  canthp1lem1  10655  xrsupss  13353  xrinfmss  13354  supxrmnf  13361  prunioo  13526  fzsuc2  13629  fzdifsuc  13631  fseq1p1m1  13645  f1resfz0f1d  13840  hashinf  14391  hashun3  14440  hashbclem  14509  relexpcnv  15098  fsumsplit1  15822  modfsummods  15871  incexclem  15916  lcmfunsnlem  16724  ramub1lem1  17111  setsid  17292  mreexexlem3d  17727  mreexexlem4d  17728  cnvtsr  18669  symgvalstruct  19498  gsumzaddlem  20022  gsummptfzsplitl  20034  dmdprdsplit2  20149  lspsnat  21306  lsppratlem3  21310  indistopon  23195  indistps  23205  indistps2  23206  ordtcnv  23395  leordtval2  23406  lecldbas  23413  cmpcld  23596  iunconn  23622  ufprim  24103  alexsubALTlem3  24243  ptcmplem1  24246  xpsdsval  24575  iccntr  25016  reconn  25023  volun  25741  voliunlem1  25746  icombl  25760  ioombl  25761  ismbf3d  25850  itgioo  26012  itgsplitioo  26034  lhop  26212  plyeq0  26405  fta1lem  26505  birthdaylem2  27154  lgsquadlem2  27582  nosepdm  27885  addscom  28196  addsproplem4  28202  addsproplem6  28204  negsproplem4  28261  negsproplem6  28263  negbdaylem  28286  mulscom  28369  mulsass  28396  usgrfilem  29714  ex-dif  30811  shjcom  31747  indifundif  32907  imadifxp  32983  difioo  33164  nn0diffz0  33176  gsummulsubdishift1  33419  symgcom  33434  pmtrcnel2  33441  cycpmcl  33467  cycpm2tr  33470  tocyccntz  33495  lindsunlem  34045  lindsun  34046  fldext2rspun  34103  ordtcnvNEW  34341  xrge0iifcnv  34354  prsiga  34552  unelldsys  34580  measun  34633  measunl  34638  difelcarsg  34732  carsgclctunlem1  34739  carsggect  34740  eulerpartgbij  34794  circlemethhgt  35062  hgt750lemb  35075  bnj1416  35459  subfacp1lem1  35692  subfacp1lem3  35695  pconnconn  35744  indispconn  35747  satfv1lem  35875  hfun  36691  onint1  37001  bj-fununsn2  37939  pibt2  38104  lindsenlbs  38307  poimirlem3  38315  poimirlem5  38317  poimirlem11  38323  poimirlem12  38324  poimirlem13  38325  poimirlem14  38326  poimirlem15  38327  poimirlem16  38328  poimirlem19  38331  poimirlem20  38332  poimirlem21  38333  poimirlem22  38334  poimirlem28  38340  poimirlem30  38342  ecuncnvepres  39085  padd02  40627  paddcom  40628  pclfinclN  40765  djhcom  42220  elrfi  43466  fzsplit1nn0  43526  eldioph2lem1  43532  eldioph2lem2  43533  diophin  43544  eldioph4b  43579  diophren  43581  kelac2  43833  pwssplit4  43857  iocunico  43979  rp-fakeuninass  44283  iunrelexp0  44469  corcltrcl  44506  frege124d  44528  mnuprdlem1  45023  equncomVD  45617  iunconnlem2  45684  snunioo1  46269  iccdifioo  46272  limciccioolb  46378  sumnnodd  46387  dirkercncflem2  46859  dirkercncflem3  46860  fourierdlem32  46894  fourierdlem93  46954  isomenndlem  47285  hoidmvlelem2  47351  hspmbllem1  47381  hspmbllem2  47382  fsumsplitsndif  48159  isubgr3stgrlem1  48772  usgrexmpl1edg  48830  usgrexmpl2edg  48835  aacllem  50662