Theorem uncom 4157

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

This proof depends on syntax axioms:   ∨ wo 861   = wceq 1569   ∈ wcel 2144   ∪ cun 4149

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-un 4151

This theorem is used by:  equncom  4158  uneq2  4161  un12  4171  un23  4172  ssun2  4177  unss2  4185  ssequn2  4187  symdifcom  4199  undir  4232  unineq  4233  dif32  4247  0un  4345  disjpss  4413  undif1  4429  undif2  4430  difcom  4443  uneqdifeq  4447  dfif4  4497  dfif5  4498  pwundif  4581  prcom  4692  tpass  4712  prprc1  4725  ssunsn2  4787  sstp  4795  unidif0OLD  5321  difxp2  6156  suc0  6440  fununfun  6588  fnunres2  6652  fresaunres2  6754  fresaunres1  6755  f1oprswap  6870  fvun2  6977  fvsnun2  7188  fsnunfv  7192  fveqf1o  7310  difex2  7774  elpwun  7783  fnsuppeq0  8209  oev2  8531  oacomf1o  8573  undifixp  8962  dfdom2  9005  domunsncan  9096  enfixsn  9105  domunsn  9146  limensuci  9172  findcard2  9180  findcard2s  9181  unfi  9186  ssfi  9188  enp1ilem  9269  frfi  9276  domunfican  9313  fsuppunbi  9381  elfiun  9422  infdifsn  9658  cantnfp1lem3  9681  rankmapu  9895  hfunOLD  9919  djuunxp  10002  infunsdom1  10290  infunsdom  10291  infxp  10292  ackbij1lem2  10298  ackbij1lem18  10314  fin1a2lem10  10487  fin1a2lem13  10490  zornn0g  10583  alephadd  10662  fpwwe2lem12  10727  canthp1lem1  10737  xrsupss  13439  xrinfmss  13440  supxrmnf  13447  prunioo  13612  fzsuc2  13716  fzdifsuc  13718  fseq1p1m1  13732  f1resfz0f1d  13927  hashinf  14479  hashun3  14528  hashbclem  14597  relexpcnv  15188  fsumsplit1  15911  modfsummods  15960  incexclem  16005  lcmfunsnlem  16816  ramub1lem1  17204  setsid  17385  mreexexlem3d  17820  mreexexlem4d  17821  cnvtsr  18762  symgvalstruct  19611  gsumzaddlem  20135  gsummptfzsplitl  20147  dmdprdsplit2  20262  lspsnat  21423  lsppratlem3  21427  lindsenlbs  22157  indistopon  23319  indistps  23329  indistps2  23330  ordtcnv  23519  leordtval2  23530  lecldbas  23537  cmpcld  23720  iunconn  23746  ufprim  24228  alexsubALTlem3  24368  ptcmplem1  24371  xpsdsval  24700  iccntr  25141  reconn  25148  volun  25866  voliunlem1  25871  icombl  25885  ioombl  25886  ismbf3d  25975  itgioo  26136  itgsplitioo  26158  lhop  26336  plyeq0  26530  fta1lem  26628  birthdaylem2  27280  lgsquadlem2  27708  nosepdm  28041  addscom  28352  addsproplem4  28358  addsproplem6  28360  negsproplem4  28417  negsproplem6  28419  negbdaylem  28442  mulscom  28525  mulsass  28552  usgrfilem  29908  ex-dif  31024  shjcom  31960  indifundif  33120  imadifxp  33195  difioo  33374  nn0diffz0  33386  gsummulsubdishift1  33629  symgcom  33644  pmtrcnel2  33651  cycpmcl  33677  cycpm2tr  33680  tocyccntz  33705  lindsunlem  34256  lindsun  34257  fldext2rspun  34314  ordtcnvNEW  34552  xrge0iifcnv  34565  prsiga  34763  unelldsys  34791  measun  34844  measunl  34849  difelcarsg  34942  carsgclctunlem1  34949  carsggect  34950  eulerpartgbij  35004  circlemethhgt  35272  hgt750lemb  35285  bnj1416  35669  subfacp1lem1  35944  subfacp1lem3  35947  pconnconn  35996  indispconn  35999  satfv1lem  36127  onint1  37237  bj-fununsn2  38176  pibt2  38341  poimirlem3  38542  poimirlem5  38544  poimirlem11  38550  poimirlem12  38551  poimirlem13  38552  poimirlem14  38553  poimirlem15  38554  poimirlem16  38555  poimirlem19  38558  poimirlem20  38559  poimirlem21  38560  poimirlem22  38561  poimirlem28  38567  poimirlem30  38569  ecuncnvepres  39328  padd02  40870  paddcom  40871  pclfinclN  41008  djhcom  42463  elrfi  43705  fzsplit1nn0  43765  eldioph2lem1  43771  eldioph2lem2  43772  diophin  43783  eldioph4b  43818  diophren  43820  kelac2  44067  pwssplit4  44091  iocunico  44213  rp-fakeuninass  44517  iunrelexp0  44702  corcltrcl  44739  frege124d  44761  mnuprdlem1  45256  equncomVD  45850  iunconnlem2  45917  snunioo1  46524  iccdifioo  46527  limciccioolb  46633  sumnnodd  46642  dirkercncflem2  47114  dirkercncflem3  47115  fourierdlem32  47149  fourierdlem93  47209  isomenndlem  47540  hoidmvlelem2  47606  hspmbllem1  47636  hspmbllem2  47637  fsumsplitsndif  48451  isubgr3stgrlem1  49064  usgrexmpl1edg  49122  usgrexmpl2edg  49127  aacllem  50939