Theorem uncom 3719

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 401	. . 3 ⊢ ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) ↔ (𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐴))
2		elun 3715	. . 3 ⊢ (𝑥 ∈ (𝐵 ∪ 𝐴) ↔ (𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐴))
3	1, 2	bitr4i 266	. 2 ⊢ ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ (𝐵 ∪ 𝐴))
4	3	uneqri 3717	1 ⊢ (𝐴 ∪ 𝐵) = (𝐵 ∪ 𝐴)

Syntax hints:   ∨ wo 382   = wceq 1475   ∈ wcel 1977   ∪ cun 3538

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-un 3545

This theorem is referenced by:  equncom  3720  uneq2  3723  un12  3733  un23  3734  ssun2  3739  unss2  3746  ssequn2  3748  symdifcom  3807  undir  3835  unineq  3836  dif32  3850  disjpss  3980  undif1  3995  undif2  3996  difcom  4005  uneqdifeq  4009  uneqdifeqOLD  4010  dfif4  4051  dfif5  4052  prcom  4211  tpass  4231  prprc1  4243  difsnid  4282  ssunsn2  4299  sspr  4306  sstp  4307  symdifv  4534  iunxdif3  4542  unidif0  4764  difxp2  5479  suc0  5716  fununfun  5848  fresaunres2  5989  fresaunres1  5990  f1oprswap  6092  fvun2  6180  fvsnun2  6354  fsnunfv  6358  fveqf1o  6457  difex2  6863  elpwun  6869  fnsuppeq0  7210  oev2  7490  oacomf1o  7532  ralxpmap  7793  undifixp  7830  dfdom2  7867  domunsncan  7945  enfixsn  7954  domunsn  7995  limensuci  8021  phplem2  8025  enp1ilem  8079  findcard2  8085  findcard2s  8086  frfi  8090  domunfican  8118  fsuppunbi  8179  elfiun  8219  infdifsn  8437  cantnfp1lem3  8460  rankmapu  8624  cdacomen  8886  infunsdom1  8918  infunsdom  8919  infxp  8920  ackbij1lem2  8926  ackbij1lem18  8942  fin1a2lem10  9114  fin1a2lem13  9117  zornn0g  9210  alephadd  9278  fpwwe2lem13  9343  canthp1lem1  9353  xrsupss  12011  xrinfmss  12012  supxrmnf  12019  prunioo  12172  fzsuc2  12268  fzdifsuc  12270  fseq1p1m1  12283  hashinf  12984  hashun3  13034  hashbclem  13093  relexpcnv  13623  modfsummods  14366  incexclem  14407  lcmfunsnlem  15192  ramub1lem1  15568  setsid  15742  mreexexlem3d  16129  mreexexlem4d  16130  cnvtsr  17045  gsumzaddlem  18144  gsummptfzsplitl  18156  dmdprdsplit2  18268  lspsnat  18966  lsppratlem3  18970  indistopon  20615  indistps  20625  indistps2  20626  ordtcnv  20815  leordtval2  20826  lecldbas  20833  cmpcld  21015  iuncon  21041  ufprim  21523  alexsubALTlem3  21663  ptcmplem1  21666  xpsdsval  21996  iccntr  22432  reconn  22439  volun  23120  voliunlem1  23125  icombl  23139  ioombl  23140  ismbf3d  23227  itgioo  23388  itgsplitioo  23410  lhop  23583  plyeq0  23771  fta1lem  23866  birthdaylem2  24479  lgsquadlem2  24906  usgrafilem1  25940  constr3pthlem1  26183  ex-dif  26672  shjcom  27601  indifundif  28740  imadifxp  28796  difioo  28934  ordtcnvNEW  29294  xrge0iifcnv  29307  prsiga  29521  unelldsys  29548  measun  29601  measunl  29606  difelcarsg  29699  carsgclctunlem1  29706  carsggect  29707  eulerpartgbij  29761  bnj1416  30361  subfacp1lem1  30415  subfacp1lem3  30418  pconcon  30467  indispcon  30470  nofulllem2  31102  hfun  31455  onint1  31618  bj-pr22val  32200  lindsenlbs  32574  poimirlem3  32582  poimirlem5  32584  poimirlem11  32590  poimirlem12  32591  poimirlem13  32592  poimirlem14  32593  poimirlem15  32594  poimirlem16  32595  poimirlem19  32598  poimirlem20  32599  poimirlem21  32600  poimirlem22  32601  poimirlem28  32607  poimirlem30  32609  padd02  34116  paddcom  34117  pclfinclN  34254  djhcom  35712  elrfi  36275  fzsplit1nn0  36335  eldioph2lem1  36341  eldioph2lem2  36342  diophin  36354  eldioph4b  36393  diophren  36395  kelac2  36653  pwssplit4  36677  iocunico  36815  rp-fakeuninass  36881  iunrelexp0  37013  corcltrcl  37050  frege124d  37072  equncomVD  38126  iunconlem2  38193  0un  38240  snunioo1  38585  iccdifioo  38588  fsumsplit1  38639  limciccioolb  38688  sumnnodd  38697  dirkercncflem2  38997  dirkercncflem3  38998  fourierdlem32  39032  fourierdlem93  39092  prsal  39214  isomenndlem  39420  hoidmvlelem2  39486  hspmbllem1  39516  hspmbllem2  39517  fsumsplitsndif  40372  usgrfilem  40546  aacllem  42356