Theorem uncom 4154

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

Syntax hints:   ∨ wo 846   = wceq 1542   ∈ wcel 2107   ∪ cun 3947

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-un 3954

This theorem is referenced by:  equncom  4155  uneq2  4158  un12  4168  un23  4169  ssun2  4174  unss2  4182  ssequn2  4184  symdifcom  4244  undir  4277  unineq  4278  dif32  4293  0un  4393  disjpss  4461  undif1  4476  undif2  4477  undifrOLD  4484  difcom  4489  uneqdifeq  4493  dfif4  4544  dfif5  4545  pwundif  4627  prcom  4737  tpass  4757  prprc1  4770  ssunsn2  4831  sspr  4837  sstp  4838  symdifv  5090  iunxdif3  5099  unidif0  5359  difxp2  6166  suc0  6440  fununfun  6597  fnunres2  6663  fresaunres2  6764  fresaunres1  6765  f1oprswap  6878  fvun2  6984  fvsnun2  7181  fsnunfv  7185  fveqf1o  7301  difex2  7747  elpwun  7756  fnsuppeq0  8177  oev2  8523  oacomf1o  8565  undifixp  8928  dfdom2  8974  domunsncan  9072  enfixsn  9081  domunsn  9127  limensuci  9153  findcard2  9164  findcard2s  9165  unfi  9172  ssfi  9173  phplem2OLD  9218  enp1ilem  9278  findcard2OLD  9284  frfi  9288  domunfican  9320  fsuppunbi  9384  elfiun  9425  infdifsn  9652  cantnfp1lem3  9675  rankmapu  9873  djuunxp  9916  infunsdom1  10208  infunsdom  10209  infxp  10210  ackbij1lem2  10216  ackbij1lem18  10232  fin1a2lem10  10404  fin1a2lem13  10407  zornn0g  10500  alephadd  10572  fpwwe2lem12  10637  canthp1lem1  10647  xrsupss  13288  xrinfmss  13289  supxrmnf  13296  prunioo  13458  fzsuc2  13559  fzdifsuc  13561  fseq1p1m1  13575  hashinf  14295  hashun3  14344  hashbclem  14411  relexpcnv  14982  fsumsplit1  15691  modfsummods  15739  incexclem  15782  lcmfunsnlem  16578  ramub1lem1  16959  setsid  17141  mreexexlem3d  17590  mreexexlem4d  17591  cnvtsr  18541  symgvalstruct  19264  symgvalstructOLD  19265  gsumzaddlem  19789  gsummptfzsplitl  19801  dmdprdsplit2  19916  lspsnat  20758  lsppratlem3  20762  indistopon  22504  indistps  22514  indistps2  22515  ordtcnv  22705  leordtval2  22716  lecldbas  22723  cmpcld  22906  iunconn  22932  ufprim  23413  alexsubALTlem3  23553  ptcmplem1  23556  xpsdsval  23887  iccntr  24337  reconn  24344  volun  25062  voliunlem1  25067  icombl  25081  ioombl  25082  ismbf3d  25171  itgioo  25333  itgsplitioo  25355  lhop  25533  plyeq0  25725  fta1lem  25820  birthdaylem2  26457  lgsquadlem2  26884  nosepdm  27187  addscom  27450  addsproplem4  27456  addsproplem6  27458  negsproplem4  27505  negsproplem6  27507  negsbdaylem  27530  mulscom  27595  mulsass  27621  usgrfilem  28584  ex-dif  29676  shjcom  30611  indifundif  31762  imadifxp  31832  difioo  31993  symgcom  32244  pmtrcnel2  32251  cycpmcl  32275  cycpm2tr  32278  tocyccntz  32303  lindsunlem  32709  lindsun  32710  ordtcnvNEW  32900  xrge0iifcnv  32913  prsiga  33129  unelldsys  33156  measun  33209  measunl  33214  difelcarsg  33309  carsgclctunlem1  33316  carsggect  33317  eulerpartgbij  33371  circlemethhgt  33655  hgt750lemb  33668  bnj1416  34050  f1resfz0f1d  34103  subfacp1lem1  34170  subfacp1lem3  34173  pconnconn  34222  indispconn  34225  satfv1lem  34353  hfun  35150  onint1  35334  bj-fununsn2  36135  pibt2  36298  lindsenlbs  36483  poimirlem3  36491  poimirlem5  36493  poimirlem11  36499  poimirlem12  36500  poimirlem13  36501  poimirlem14  36502  poimirlem15  36503  poimirlem16  36504  poimirlem19  36507  poimirlem20  36508  poimirlem21  36509  poimirlem22  36510  poimirlem28  36516  poimirlem30  36518  padd02  38683  paddcom  38684  pclfinclN  38821  djhcom  40276  metakunt24  41008  elrfi  41432  fzsplit1nn0  41492  eldioph2lem1  41498  eldioph2lem2  41499  diophin  41510  eldioph4b  41549  diophren  41551  kelac2  41807  pwssplit4  41831  iocunico  41960  rp-fakeuninass  42267  iunrelexp0  42453  corcltrcl  42490  frege124d  42512  mnuprdlem1  43031  equncomVD  43629  iunconnlem2  43696  snunioo1  44225  iccdifioo  44228  limciccioolb  44337  sumnnodd  44346  dirkercncflem2  44820  dirkercncflem3  44821  fourierdlem32  44855  fourierdlem93  44915  isomenndlem  45246  hoidmvlelem2  45312  hspmbllem1  45342  hspmbllem2  45343  fsumsplitsndif  46041  aacllem  47848