Theorem uncom 4133

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 870	. . 3 ⊢ ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) ↔ (𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐴))
2		elun 4128	. . 3 ⊢ (𝑥 ∈ (𝐵 ∪ 𝐴) ↔ (𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐴))
3	1, 2	bitr4i 278	. 2 ⊢ ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ (𝐵 ∪ 𝐴))
4	3	uneqri 4131	1 ⊢ (𝐴 ∪ 𝐵) = (𝐵 ∪ 𝐴)

Syntax hints:   ∨ wo 847   = wceq 1540   ∈ wcel 2108   ∪ cun 3924

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-v 3461  df-un 3931

This theorem is referenced by:  equncom  4134  uneq2  4137  un12  4148  un23  4149  ssun2  4154  unss2  4162  ssequn2  4164  symdifcom  4229  undir  4262  unineq  4263  dif32  4277  0un  4371  disjpss  4436  undif1  4451  undif2  4452  undifrOLD  4459  difcom  4464  uneqdifeq  4468  dfif4  4516  dfif5  4517  pwundif  4599  prcom  4708  tpass  4728  prprc1  4741  ssunsn2  4803  sspr  4811  sstp  4812  symdifv  5062  iunxdif3  5071  unidif0  5330  difxp2  6155  suc0  6428  fununfun  6583  fnunres2  6650  fresaunres2  6749  fresaunres1  6750  f1oprswap  6861  fvun2  6970  fvsnun2  7174  fsnunfv  7178  fveqf1o  7294  difex2  7752  elpwun  7761  fnsuppeq0  8189  oev2  8533  oacomf1o  8575  undifixp  8946  dfdom2  8990  domunsncan  9084  enfixsn  9093  domunsn  9139  limensuci  9165  findcard2  9176  findcard2s  9177  unfi  9183  ssfi  9185  phplem2OLD  9227  enp1ilem  9282  frfi  9291  domunfican  9331  fsuppunbi  9399  elfiun  9440  infdifsn  9669  cantnfp1lem3  9692  rankmapu  9890  djuunxp  9933  infunsdom1  10224  infunsdom  10225  infxp  10226  ackbij1lem2  10232  ackbij1lem18  10248  fin1a2lem10  10421  fin1a2lem13  10424  zornn0g  10517  alephadd  10589  fpwwe2lem12  10654  canthp1lem1  10664  xrsupss  13323  xrinfmss  13324  supxrmnf  13331  prunioo  13496  fzsuc2  13597  fzdifsuc  13599  fseq1p1m1  13613  hashinf  14351  hashun3  14400  hashbclem  14468  relexpcnv  15052  fsumsplit1  15759  modfsummods  15807  incexclem  15850  lcmfunsnlem  16658  ramub1lem1  17044  setsid  17224  mreexexlem3d  17656  mreexexlem4d  17657  cnvtsr  18596  symgvalstruct  19376  gsumzaddlem  19900  gsummptfzsplitl  19912  dmdprdsplit2  20027  lspsnat  21104  lsppratlem3  21108  indistopon  22937  indistps  22947  indistps2  22948  ordtcnv  23137  leordtval2  23148  lecldbas  23155  cmpcld  23338  iunconn  23364  ufprim  23845  alexsubALTlem3  23985  ptcmplem1  23988  xpsdsval  24318  iccntr  24759  reconn  24766  volun  25496  voliunlem1  25501  icombl  25515  ioombl  25516  ismbf3d  25605  itgioo  25767  itgsplitioo  25789  lhop  25971  plyeq0  26166  fta1lem  26265  birthdaylem2  26912  lgsquadlem2  27342  nosepdm  27646  addscom  27916  addsproplem4  27922  addsproplem6  27924  negsproplem4  27980  negsproplem6  27982  negsbdaylem  28005  mulscom  28082  mulsass  28109  usgrfilem  29252  ex-dif  30350  shjcom  31285  indifundif  32451  imadifxp  32528  difioo  32705  symgcom  33040  pmtrcnel2  33047  cycpmcl  33073  cycpm2tr  33076  tocyccntz  33101  lindsunlem  33610  lindsun  33611  fldext2rspun  33669  ordtcnvNEW  33897  xrge0iifcnv  33910  prsiga  34108  unelldsys  34135  measun  34188  measunl  34193  difelcarsg  34288  carsgclctunlem1  34295  carsggect  34296  eulerpartgbij  34350  circlemethhgt  34621  hgt750lemb  34634  bnj1416  35016  f1resfz0f1d  35082  subfacp1lem1  35147  subfacp1lem3  35150  pconnconn  35199  indispconn  35202  satfv1lem  35330  hfun  36142  onint1  36413  bj-fununsn2  37218  pibt2  37381  lindsenlbs  37585  poimirlem3  37593  poimirlem5  37595  poimirlem11  37601  poimirlem12  37602  poimirlem13  37603  poimirlem14  37604  poimirlem15  37605  poimirlem16  37606  poimirlem19  37609  poimirlem20  37610  poimirlem21  37611  poimirlem22  37612  poimirlem28  37618  poimirlem30  37620  padd02  39777  paddcom  39778  pclfinclN  39915  djhcom  41370  metakunt24  42187  elrfi  42664  fzsplit1nn0  42724  eldioph2lem1  42730  eldioph2lem2  42731  diophin  42742  eldioph4b  42781  diophren  42783  kelac2  43036  pwssplit4  43060  iocunico  43182  rp-fakeuninass  43487  iunrelexp0  43673  corcltrcl  43710  frege124d  43732  mnuprdlem1  44244  equncomVD  44840  iunconnlem2  44907  snunioo1  45489  iccdifioo  45492  limciccioolb  45598  sumnnodd  45607  dirkercncflem2  46081  dirkercncflem3  46082  fourierdlem32  46116  fourierdlem93  46176  isomenndlem  46507  hoidmvlelem2  46573  hspmbllem1  46603  hspmbllem2  46604  fsumsplitsndif  47335  isubgr3stgrlem1  47926  usgrexmpl1edg  47976  usgrexmpl2edg  47981  aacllem  49613