Theorem uncom 4113

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

Syntax hints:   ∨ wo 860   = wceq 1570   ∈ wcel 2143   ∪ cun 3904

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-un 3911

This theorem is referenced by:  equncom  4114  uneq2  4117  un12  4127  un23  4128  ssun2  4133  unss2  4141  ssequn2  4143  symdifcom  4208  undir  4241  unineq  4242  dif32  4256  0un  4354  disjpss  4422  undif1  4438  undif2  4439  difcom  4450  uneqdifeq  4454  dfif4  4504  dfif5  4505  pwundif  4588  prcom  4699  tpass  4719  prprc1  4732  ssunsn2  4794  sstp  4802  unidif0OLD  5333  difxp2  6165  suc0  6440  fununfun  6586  fnunres2  6650  fresaunres2  6752  fresaunres1  6753  f1oprswap  6868  fvun2  6975  fvsnun2  7183  fsnunfv  7187  fveqf1o  7302  difex2  7760  elpwun  7769  fnsuppeq0  8189  oev2  8509  oacomf1o  8551  undifixp  8933  dfdom2  8976  domunsncan  9066  enfixsn  9075  domunsn  9116  limensuci  9142  findcard2  9150  findcard2s  9151  unfi  9156  ssfi  9158  enp1ilem  9239  frfi  9246  domunfican  9282  fsuppunbi  9350  elfiun  9391  infdifsn  9627  cantnfp1lem3  9650  rankmapu  9851  djuunxp  9908  infunsdom1  10196  infunsdom  10197  infxp  10198  ackbij1lem2  10204  ackbij1lem18  10220  fin1a2lem10  10394  fin1a2lem13  10397  zornn0g  10490  alephadd  10563  fpwwe2lem12  10628  canthp1lem1  10638  xrsupss  13336  xrinfmss  13337  supxrmnf  13344  prunioo  13509  fzsuc2  13612  fzdifsuc  13614  fseq1p1m1  13628  hashinf  14373  hashun3  14422  hashbclem  14491  relexpcnv  15074  fsumsplit1  15798  modfsummods  15847  incexclem  15892  lcmfunsnlem  16700  ramub1lem1  17087  setsid  17268  mreexexlem3d  17703  mreexexlem4d  17704  cnvtsr  18645  symgvalstruct  19468  gsumzaddlem  19992  gsummptfzsplitl  20004  dmdprdsplit2  20119  lspsnat  21250  lsppratlem3  21254  indistopon  23139  indistps  23149  indistps2  23150  ordtcnv  23339  leordtval2  23350  lecldbas  23357  cmpcld  23540  iunconn  23566  ufprim  24047  alexsubALTlem3  24187  ptcmplem1  24190  xpsdsval  24519  iccntr  24960  reconn  24967  volun  25685  voliunlem1  25690  icombl  25704  ioombl  25705  ismbf3d  25794  itgioo  25956  itgsplitioo  25978  lhop  26156  plyeq0  26349  fta1lem  26449  birthdaylem2  27098  lgsquadlem2  27526  nosepdm  27829  addscom  28140  addsproplem4  28146  addsproplem6  28148  negsproplem4  28205  negsproplem6  28207  negbdaylem  28230  mulscom  28313  mulsass  28340  usgrfilem  29658  ex-dif  30755  shjcom  31691  indifundif  32851  imadifxp  32927  difioo  33108  nn0diffz0  33120  gsummulsubdishift1  33369  symgcom  33384  pmtrcnel2  33391  cycpmcl  33417  cycpm2tr  33420  tocyccntz  33445  lindsunlem  33995  lindsun  33996  fldext2rspun  34053  ordtcnvNEW  34291  xrge0iifcnv  34304  prsiga  34502  unelldsys  34529  measun  34582  measunl  34587  difelcarsg  34681  carsgclctunlem1  34688  carsggect  34689  eulerpartgbij  34743  circlemethhgt  35011  hgt750lemb  35024  bnj1416  35408  f1resfz0f1d  35586  subfacp1lem1  35652  subfacp1lem3  35655  pconnconn  35704  indispconn  35707  satfv1lem  35835  hfun  36651  onint1  36941  bj-fununsn2  37879  pibt2  38044  lindsenlbs  38247  poimirlem3  38255  poimirlem5  38257  poimirlem11  38263  poimirlem12  38264  poimirlem13  38265  poimirlem14  38266  poimirlem15  38267  poimirlem16  38268  poimirlem19  38271  poimirlem20  38272  poimirlem21  38273  poimirlem22  38274  poimirlem28  38280  poimirlem30  38282  ecuncnvepres  39025  padd02  40567  paddcom  40568  pclfinclN  40705  djhcom  42160  elrfi  43408  fzsplit1nn0  43468  eldioph2lem1  43474  eldioph2lem2  43475  diophin  43486  eldioph4b  43521  diophren  43523  kelac2  43775  pwssplit4  43799  iocunico  43921  rp-fakeuninass  44225  iunrelexp0  44411  corcltrcl  44448  frege124d  44470  mnuprdlem1  44965  equncomVD  45559  iunconnlem2  45626  snunioo1  46211  iccdifioo  46214  limciccioolb  46320  sumnnodd  46329  dirkercncflem2  46801  dirkercncflem3  46802  fourierdlem32  46836  fourierdlem93  46896  isomenndlem  47227  hoidmvlelem2  47293  hspmbllem1  47323  hspmbllem2  47324  fsumsplitsndif  48101  isubgr3stgrlem1  48714  usgrexmpl1edg  48772  usgrexmpl2edg  48777  aacllem  50584