Theorem uncom 4153

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 868	. . 3 ⊢ ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) ↔ (𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐴))
2		elun 4148	. . 3 ⊢ (𝑥 ∈ (𝐵 ∪ 𝐴) ↔ (𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐴))
3	1, 2	bitr4i 277	. 2 ⊢ ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ (𝐵 ∪ 𝐴))
4	3	uneqri 4151	1 ⊢ (𝐴 ∪ 𝐵) = (𝐵 ∪ 𝐴)

Syntax hints:   ∨ wo 845   = wceq 1534   ∈ wcel 2099   ∪ cun 3945

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2697

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2704  df-cleq 2718  df-clel 2803  df-v 3464  df-un 3952

This theorem is referenced by:  equncom  4154  uneq2  4157  un12  4168  un23  4169  ssun2  4174  unss2  4182  ssequn2  4184  symdifcom  4245  undir  4278  unineq  4279  dif32  4294  0un  4397  disjpss  4465  undif1  4480  undif2  4481  undifrOLD  4488  difcom  4493  uneqdifeq  4497  dfif4  4548  dfif5  4549  pwundif  4631  prcom  4741  tpass  4761  prprc1  4774  ssunsn2  4836  sspr  4842  sstp  4843  symdifv  5094  iunxdif3  5103  unidif0  5364  difxp2  6177  suc0  6451  fununfun  6607  fnunres2  6673  fresaunres2  6774  fresaunres1  6775  f1oprswap  6887  fvun2  6994  fvsnun2  7197  fsnunfv  7201  fveqf1o  7316  difex2  7768  elpwun  7777  fnsuppeq0  8206  oev2  8553  oacomf1o  8595  undifixp  8963  dfdom2  9009  domunsncan  9110  enfixsn  9119  domunsn  9165  limensuci  9191  findcard2  9202  findcard2s  9203  unfi  9210  ssfi  9211  phplem2OLD  9252  enp1ilem  9312  findcard2OLD  9318  frfi  9322  domunfican  9363  fsuppunbi  9432  elfiun  9473  infdifsn  9700  cantnfp1lem3  9723  rankmapu  9921  djuunxp  9964  infunsdom1  10256  infunsdom  10257  infxp  10258  ackbij1lem2  10264  ackbij1lem18  10280  fin1a2lem10  10452  fin1a2lem13  10455  zornn0g  10548  alephadd  10620  fpwwe2lem12  10685  canthp1lem1  10695  xrsupss  13342  xrinfmss  13343  supxrmnf  13350  prunioo  13512  fzsuc2  13613  fzdifsuc  13615  fseq1p1m1  13629  hashinf  14352  hashun3  14401  hashbclem  14469  relexpcnv  15040  fsumsplit1  15749  modfsummods  15797  incexclem  15840  lcmfunsnlem  16642  ramub1lem1  17028  setsid  17210  mreexexlem3d  17659  mreexexlem4d  17660  cnvtsr  18613  symgvalstruct  19394  symgvalstructOLD  19395  gsumzaddlem  19919  gsummptfzsplitl  19931  dmdprdsplit2  20046  lspsnat  21126  lsppratlem3  21130  indistopon  22995  indistps  23005  indistps2  23006  ordtcnv  23196  leordtval2  23207  lecldbas  23214  cmpcld  23397  iunconn  23423  ufprim  23904  alexsubALTlem3  24044  ptcmplem1  24047  xpsdsval  24378  iccntr  24828  reconn  24835  volun  25565  voliunlem1  25570  icombl  25584  ioombl  25585  ismbf3d  25674  itgioo  25836  itgsplitioo  25858  lhop  26040  plyeq0  26238  fta1lem  26335  birthdaylem2  26980  lgsquadlem2  27410  nosepdm  27714  addscom  27980  addsproplem4  27986  addsproplem6  27988  negsproplem4  28040  negsproplem6  28042  negsbdaylem  28065  mulscom  28140  mulsass  28167  usgrfilem  29263  ex-dif  30356  shjcom  31291  indifundif  32451  imadifxp  32521  difioo  32684  symgcom  32961  pmtrcnel2  32968  cycpmcl  32994  cycpm2tr  32997  tocyccntz  33022  lindsunlem  33519  lindsun  33520  ordtcnvNEW  33735  xrge0iifcnv  33748  prsiga  33964  unelldsys  33991  measun  34044  measunl  34049  difelcarsg  34144  carsgclctunlem1  34151  carsggect  34152  eulerpartgbij  34206  circlemethhgt  34489  hgt750lemb  34502  bnj1416  34884  f1resfz0f1d  34941  subfacp1lem1  35007  subfacp1lem3  35010  pconnconn  35059  indispconn  35062  satfv1lem  35190  hfun  36002  onint1  36161  bj-fununsn2  36961  pibt2  37124  lindsenlbs  37316  poimirlem3  37324  poimirlem5  37326  poimirlem11  37332  poimirlem12  37333  poimirlem13  37334  poimirlem14  37335  poimirlem15  37336  poimirlem16  37337  poimirlem19  37340  poimirlem20  37341  poimirlem21  37342  poimirlem22  37343  poimirlem28  37349  poimirlem30  37351  padd02  39511  paddcom  39512  pclfinclN  39649  djhcom  41104  metakunt24  41914  elrfi  42351  fzsplit1nn0  42411  eldioph2lem1  42417  eldioph2lem2  42418  diophin  42429  eldioph4b  42468  diophren  42470  kelac2  42726  pwssplit4  42750  iocunico  42876  rp-fakeuninass  43183  iunrelexp0  43369  corcltrcl  43406  frege124d  43428  mnuprdlem1  43946  equncomVD  44544  iunconnlem2  44611  snunioo1  45130  iccdifioo  45133  limciccioolb  45242  sumnnodd  45251  dirkercncflem2  45725  dirkercncflem3  45726  fourierdlem32  45760  fourierdlem93  45820  isomenndlem  46151  hoidmvlelem2  46217  hspmbllem1  46247  hspmbllem2  46248  fsumsplitsndif  46945  aacllem  48549