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  4582  prcom  4689  tpass  4709  prprc1  4722  ssunsn2  4782  sstp  4790  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  8212  oev2  8534  oacomf1o  8576  undifixp  8965  dfdom2  9008  domunsncan  9099  enfixsn  9108  domunsn  9149  limensuci  9175  findcard2  9183  findcard2s  9184  unfi  9189  ssfi  9191  enp1ilem  9272  frfi  9279  domunfican  9316  fsuppunbi  9384  elfiun  9425  infdifsn  9661  cantnfp1lem3  9684  rankmapu  9898  hfunOLD  9922  djuunxp  10005  infunsdom1  10293  infunsdom  10294  infxp  10295  ackbij1lem2  10301  ackbij1lem18  10317  fin1a2lem10  10490  fin1a2lem13  10493  zornn0g  10586  alephadd  10665  fpwwe2lem12  10730  canthp1lem1  10740  xrsupss  13442  xrinfmss  13443  supxrmnf  13450  prunioo  13615  fzsuc2  13719  fzdifsuc  13721  fseq1p1m1  13735  f1resfz0f1d  13930  hashinf  14482  hashun3  14531  hashbclem  14600  relexpcnv  15193  fsumsplit1  15916  modfsummods  15965  incexclem  16010  lcmfunsnlem  16821  ramub1lem1  17209  setsid  17390  mreexexlem3d  17825  mreexexlem4d  17826  cnvtsr  18767  symgvalstruct  19616  gsumzaddlem  20140  gsummptfzsplitl  20152  dmdprdsplit2  20267  lspsnat  21428  lsppratlem3  21432  lindsenlbs  22162  indistopon  23324  indistps  23334  indistps2  23335  ordtcnv  23524  leordtval2  23535  lecldbas  23542  cmpcld  23725  iunconn  23751  ufprim  24233  alexsubALTlem3  24373  ptcmplem1  24376  xpsdsval  24705  iccntr  25146  reconn  25153  volun  25871  voliunlem1  25876  icombl  25890  ioombl  25891  ismbf3d  25980  itgioo  26141  itgsplitioo  26163  lhop  26341  plyeq0  26535  fta1lem  26633  birthdaylem2  27285  lgsquadlem2  27713  nosepdm  28046  addscom  28357  addsproplem4  28363  addsproplem6  28365  negsproplem4  28422  negsproplem6  28424  negbdaylem  28447  mulscom  28530  mulsass  28557  usgrfilem  29913  ex-dif  31029  shjcom  31965  indifundif  33167  imadifxp  33242  difioo  33420  nn0diffz0  33432  gsummulsubdishift1  33675  symgcom  33690  pmtrcnel2  33697  cycpmcl  33723  cycpm2tr  33726  tocyccntz  33751  lindsunlem  34302  lindsun  34303  fldext2rspun  34360  ordtcnvNEW  34598  xrge0iifcnv  34611  prsiga  34809  unelldsys  34837  measun  34890  measunl  34895  difelcarsg  34988  carsgclctunlem1  34995  carsggect  34996  eulerpartgbij  35050  circlemethhgt  35318  hgt750lemb  35331  bnj1416  35715  subfacp1lem1  36030  subfacp1lem3  36033  pconnconn  36082  indispconn  36085  satfv1lem  36213  onint1  37329  bj-fununsn2  38268  pibt2  38433  poimirlem3  38634  poimirlem5  38636  poimirlem11  38642  poimirlem12  38643  poimirlem13  38644  poimirlem14  38645  poimirlem15  38646  poimirlem16  38647  poimirlem19  38650  poimirlem20  38651  poimirlem21  38652  poimirlem22  38653  poimirlem28  38659  poimirlem30  38661  ecuncnvepres  39420  padd02  40962  paddcom  40963  pclfinclN  41100  djhcom  42555  elrfi  43798  fzsplit1nn0  43858  eldioph2lem1  43864  eldioph2lem2  43865  diophin  43876  eldioph4b  43911  diophren  43913  kelac2  44160  pwssplit4  44184  iocunico  44306  rp-fakeuninass  44610  iunrelexp0  44795  corcltrcl  44832  frege124d  44854  mnuprdlem1  45349  equncomVD  45943  iunconnlem2  46010  snunioo1  46617  iccdifioo  46620  limciccioolb  46726  sumnnodd  46735  dirkercncflem2  47207  dirkercncflem3  47208  fourierdlem32  47242  fourierdlem93  47302  isomenndlem  47633  hoidmvlelem2  47699  hspmbllem1  47729  hspmbllem2  47730  fsumsplitsndif  48544  isubgr3stgrlem1  49157  usgrexmpl1edg  49215  usgrexmpl2edg  49220  aacllem  51107