Theorem uncom 4124

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

Syntax hints:   ∨ wo 847   = wceq 1540   ∈ wcel 2109   ∪ cun 3915

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 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-v 3452  df-un 3922

This theorem is referenced by:  equncom  4125  uneq2  4128  un12  4139  un23  4140  ssun2  4145  unss2  4153  ssequn2  4155  symdifcom  4220  undir  4253  unineq  4254  dif32  4268  0un  4362  disjpss  4427  undif1  4442  undif2  4443  undifrOLD  4450  difcom  4455  uneqdifeq  4459  dfif4  4507  dfif5  4508  pwundif  4590  prcom  4699  tpass  4719  prprc1  4732  ssunsn2  4794  sspr  4802  sstp  4803  symdifv  5053  iunxdif3  5062  unidif0  5318  difxp2  6142  suc0  6412  fununfun  6567  fnunres2  6634  fresaunres2  6735  fresaunres1  6736  f1oprswap  6847  fvun2  6956  fvsnun2  7160  fsnunfv  7164  fveqf1o  7280  difex2  7739  elpwun  7748  fnsuppeq0  8174  oev2  8490  oacomf1o  8532  undifixp  8910  dfdom2  8952  domunsncan  9046  enfixsn  9055  domunsn  9097  limensuci  9123  findcard2  9134  findcard2s  9135  unfi  9141  ssfi  9143  enp1ilem  9230  frfi  9239  domunfican  9279  fsuppunbi  9347  elfiun  9388  infdifsn  9617  cantnfp1lem3  9640  rankmapu  9838  djuunxp  9881  infunsdom1  10172  infunsdom  10173  infxp  10174  ackbij1lem2  10180  ackbij1lem18  10196  fin1a2lem10  10369  fin1a2lem13  10372  zornn0g  10465  alephadd  10537  fpwwe2lem12  10602  canthp1lem1  10612  xrsupss  13276  xrinfmss  13277  supxrmnf  13284  prunioo  13449  fzsuc2  13550  fzdifsuc  13552  fseq1p1m1  13566  hashinf  14307  hashun3  14356  hashbclem  14424  relexpcnv  15008  fsumsplit1  15718  modfsummods  15766  incexclem  15809  lcmfunsnlem  16618  ramub1lem1  17004  setsid  17184  mreexexlem3d  17614  mreexexlem4d  17615  cnvtsr  18554  symgvalstruct  19334  gsumzaddlem  19858  gsummptfzsplitl  19870  dmdprdsplit2  19985  lspsnat  21062  lsppratlem3  21066  indistopon  22895  indistps  22905  indistps2  22906  ordtcnv  23095  leordtval2  23106  lecldbas  23113  cmpcld  23296  iunconn  23322  ufprim  23803  alexsubALTlem3  23943  ptcmplem1  23946  xpsdsval  24276  iccntr  24717  reconn  24724  volun  25453  voliunlem1  25458  icombl  25472  ioombl  25473  ismbf3d  25562  itgioo  25724  itgsplitioo  25746  lhop  25928  plyeq0  26123  fta1lem  26222  birthdaylem2  26869  lgsquadlem2  27299  nosepdm  27603  addscom  27880  addsproplem4  27886  addsproplem6  27888  negsproplem4  27944  negsproplem6  27946  negsbdaylem  27969  mulscom  28049  mulsass  28076  usgrfilem  29261  ex-dif  30359  shjcom  31294  indifundif  32460  imadifxp  32537  difioo  32712  symgcom  33047  pmtrcnel2  33054  cycpmcl  33080  cycpm2tr  33083  tocyccntz  33108  lindsunlem  33627  lindsun  33628  fldext2rspun  33684  ordtcnvNEW  33917  xrge0iifcnv  33930  prsiga  34128  unelldsys  34155  measun  34208  measunl  34213  difelcarsg  34308  carsgclctunlem1  34315  carsggect  34316  eulerpartgbij  34370  circlemethhgt  34641  hgt750lemb  34654  bnj1416  35036  f1resfz0f1d  35108  subfacp1lem1  35173  subfacp1lem3  35176  pconnconn  35225  indispconn  35228  satfv1lem  35356  hfun  36173  onint1  36444  bj-fununsn2  37249  pibt2  37412  lindsenlbs  37616  poimirlem3  37624  poimirlem5  37626  poimirlem11  37632  poimirlem12  37633  poimirlem13  37634  poimirlem14  37635  poimirlem15  37636  poimirlem16  37637  poimirlem19  37640  poimirlem20  37641  poimirlem21  37642  poimirlem22  37643  poimirlem28  37649  poimirlem30  37651  padd02  39813  paddcom  39814  pclfinclN  39951  djhcom  41406  elrfi  42689  fzsplit1nn0  42749  eldioph2lem1  42755  eldioph2lem2  42756  diophin  42767  eldioph4b  42806  diophren  42808  kelac2  43061  pwssplit4  43085  iocunico  43207  rp-fakeuninass  43512  iunrelexp0  43698  corcltrcl  43735  frege124d  43757  mnuprdlem1  44268  equncomVD  44864  iunconnlem2  44931  snunioo1  45517  iccdifioo  45520  limciccioolb  45626  sumnnodd  45635  dirkercncflem2  46109  dirkercncflem3  46110  fourierdlem32  46144  fourierdlem93  46204  isomenndlem  46535  hoidmvlelem2  46601  hspmbllem1  46631  hspmbllem2  46632  fsumsplitsndif  47378  isubgr3stgrlem1  47969  usgrexmpl1edg  48019  usgrexmpl2edg  48024  aacllem  49794