Theorem uncom 3757

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 402	. . 3 ⊢ ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) ↔ (𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐴))
2		elun 3753	. . 3 ⊢ (𝑥 ∈ (𝐵 ∪ 𝐴) ↔ (𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐴))
3	1, 2	bitr4i 267	. 2 ⊢ ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ (𝐵 ∪ 𝐴))
4	3	uneqri 3755	1 ⊢ (𝐴 ∪ 𝐵) = (𝐵 ∪ 𝐴)

Syntax hints:   ∨ wo 383   = wceq 1483   ∈ wcel 1990   ∪ cun 3572

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-un 3579

This theorem is referenced by:  equncom  3758  uneq2  3761  un12  3771  un23  3772  ssun2  3777  unss2  3784  ssequn2  3786  symdifcom  3845  undir  3876  unineq  3877  dif32  3891  disjpss  4028  undif1  4043  undif2  4044  difcom  4053  uneqdifeq  4057  uneqdifeqOLD  4058  dfif4  4101  dfif5  4102  prcom  4267  tpass  4287  prprc1  4300  difsnid  4341  ssunsn2  4359  sspr  4366  sstp  4367  symdifv  4598  iunxdif3  4606  unidif0  4838  difxp2  5560  suc0  5799  fununfun  5934  fresaunres2  6076  fresaunres1  6077  f1oprswap  6180  fvun2  6270  fvsnun2  6449  fsnunfv  6453  fveqf1o  6557  difex2  6969  elpwun  6977  fnsuppeq0  7323  oev2  7603  oacomf1o  7645  ralxpmap  7907  undifixp  7944  dfdom2  7981  domunsncan  8060  enfixsn  8069  domunsn  8110  limensuci  8136  phplem2  8140  enp1ilem  8194  findcard2  8200  findcard2s  8201  frfi  8205  domunfican  8233  fsuppunbi  8296  elfiun  8336  infdifsn  8554  cantnfp1lem3  8577  rankmapu  8741  cdacomen  9003  infunsdom1  9035  infunsdom  9036  infxp  9037  ackbij1lem2  9043  ackbij1lem18  9059  fin1a2lem10  9231  fin1a2lem13  9234  zornn0g  9327  alephadd  9399  fpwwe2lem13  9464  canthp1lem1  9474  xrsupss  12139  xrinfmss  12140  supxrmnf  12147  prunioo  12301  fzsuc2  12398  fzdifsuc  12400  fseq1p1m1  12414  hashinf  13122  hashun3  13173  hashbclem  13236  relexpcnv  13775  modfsummods  14525  incexclem  14568  lcmfunsnlem  15354  ramub1lem1  15730  setsid  15914  mreexexlem3d  16306  mreexexlem4d  16307  cnvtsr  17222  gsumzaddlem  18321  gsummptfzsplitl  18333  dmdprdsplit2  18445  lspsnat  19145  lsppratlem3  19149  indistopon  20805  indistps  20815  indistps2  20816  ordtcnv  21005  leordtval2  21016  lecldbas  21023  cmpcld  21205  iunconn  21231  ufprim  21713  alexsubALTlem3  21853  ptcmplem1  21856  xpsdsval  22186  iccntr  22624  reconn  22631  volun  23313  voliunlem1  23318  icombl  23332  ioombl  23333  ismbf3d  23421  itgioo  23582  itgsplitioo  23604  lhop  23779  plyeq0  23967  fta1lem  24062  birthdaylem2  24679  lgsquadlem2  25106  usgrfilem  26219  ex-dif  27280  shjcom  28217  indifundif  29356  imadifxp  29414  difioo  29544  ordtcnvNEW  29966  xrge0iifcnv  29979  prsiga  30194  unelldsys  30221  measun  30274  measunl  30279  difelcarsg  30372  carsgclctunlem1  30379  carsggect  30380  eulerpartgbij  30434  circlemethhgt  30721  hgt750lemb  30734  bnj1416  31107  subfacp1lem1  31161  subfacp1lem3  31164  pconnconn  31213  indispconn  31216  nosepdm  31834  hfun  32285  onint1  32448  bj-pr22val  33007  lindsenlbs  33404  poimirlem3  33412  poimirlem5  33414  poimirlem11  33420  poimirlem12  33421  poimirlem13  33422  poimirlem14  33423  poimirlem15  33424  poimirlem16  33425  poimirlem19  33428  poimirlem20  33429  poimirlem21  33430  poimirlem22  33431  poimirlem28  33437  poimirlem30  33439  padd02  35098  paddcom  35099  pclfinclN  35236  djhcom  36694  elrfi  37257  fzsplit1nn0  37317  eldioph2lem1  37323  eldioph2lem2  37324  diophin  37336  eldioph4b  37375  diophren  37377  kelac2  37635  pwssplit4  37659  iocunico  37796  rp-fakeuninass  37862  iunrelexp0  37994  corcltrcl  38031  frege124d  38053  equncomVD  39104  iunconnlem2  39171  0un  39215  snunioo1  39738  iccdifioo  39741  fsumsplit1  39804  limciccioolb  39853  sumnnodd  39862  dirkercncflem2  40321  dirkercncflem3  40322  fourierdlem32  40356  fourierdlem93  40416  prsal  40538  isomenndlem  40744  hoidmvlelem2  40810  hspmbllem1  40840  hspmbllem2  40841  fsumsplitsndif  41343  aacllem  42547