Theorem uncom 4095

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 876	. . 3 ⊢ ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) ↔ (𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐴))
2		elun 4090	. . 3 ⊢ (𝑥 ∈ (𝐵 ∪ 𝐴) ↔ (𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐴))
3	1, 2	bitr4i 279	. 2 ⊢ ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ (𝐵 ∪ 𝐴))
4	3	uneqri 4093	1 ⊢ (𝐴 ∪ 𝐵) = (𝐵 ∪ 𝐴)

Syntax hints:   ∨ wo 853   = wceq 1547   ∈ wcel 2119   ∪ cun 3888

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-v 3434  df-un 3895

This theorem is referenced by:  equncom  4096  uneq2  4099  un12  4109  un23  4110  ssun2  4115  unss2  4123  ssequn2  4125  symdifcom  4189  undir  4222  unineq  4223  dif32  4237  0un  4331  disjpss  4396  undif1  4411  undif2  4412  difcom  4423  uneqdifeq  4427  dfif4  4477  dfif5  4478  pwundif  4560  prcom  4671  tpass  4691  prprc1  4704  ssunsn2  4765  sstp  4774  unidif0OLD  5296  difxp2  6124  suc0  6394  fununfun  6540  fnunres2  6605  fresaunres2  6706  fresaunres1  6707  f1oprswap  6819  fvun2  6926  fvsnun2  7134  fsnunfv  7138  fveqf1o  7253  difex2  7710  elpwun  7719  fnsuppeq0  8139  oev2  8455  oacomf1o  8497  undifixp  8879  dfdom2  8922  domunsncan  9012  enfixsn  9021  domunsn  9062  limensuci  9088  findcard2  9096  findcard2s  9097  unfi  9102  ssfi  9104  enp1ilem  9185  frfi  9192  domunfican  9229  fsuppunbi  9299  elfiun  9340  infdifsn  9576  cantnfp1lem3  9599  rankmapu  9800  djuunxp  9843  infunsdom1  10132  infunsdom  10133  infxp  10134  ackbij1lem2  10140  ackbij1lem18  10156  fin1a2lem10  10329  fin1a2lem13  10332  zornn0g  10425  alephadd  10498  fpwwe2lem12  10563  canthp1lem1  10573  xrsupss  13259  xrinfmss  13260  supxrmnf  13267  prunioo  13432  fzsuc2  13534  fzdifsuc  13536  fseq1p1m1  13550  hashinf  14295  hashun3  14344  hashbclem  14412  relexpcnv  14995  fsumsplit1  15705  modfsummods  15754  incexclem  15799  lcmfunsnlem  16608  ramub1lem1  16995  setsid  17175  mreexexlem3d  17610  mreexexlem4d  17611  cnvtsr  18552  symgvalstruct  19370  gsumzaddlem  19894  gsummptfzsplitl  19906  dmdprdsplit2  20021  lspsnat  21145  lsppratlem3  21149  indistopon  22991  indistps  23001  indistps2  23002  ordtcnv  23191  leordtval2  23202  lecldbas  23209  cmpcld  23392  iunconn  23418  ufprim  23899  alexsubALTlem3  24039  ptcmplem1  24042  xpsdsval  24371  iccntr  24812  reconn  24819  volun  25537  voliunlem1  25542  icombl  25556  ioombl  25557  ismbf3d  25646  itgioo  25808  itgsplitioo  25830  lhop  26008  plyeq0  26201  fta1lem  26298  birthdaylem2  26941  lgsquadlem2  27369  nosepdm  27673  addscom  27983  addsproplem4  27989  addsproplem6  27991  negsproplem4  28048  negsproplem6  28050  negbdaylem  28073  mulscom  28156  mulsass  28183  usgrfilem  29421  ex-dif  30518  shjcom  31454  indifundif  32619  imadifxp  32697  difioo  32881  nn0diffz0  32893  gsummulsubdishift1  33156  symgcom  33171  pmtrcnel2  33178  cycpmcl  33204  cycpm2tr  33207  tocyccntz  33232  lindsunlem  33815  lindsun  33816  fldext2rspun  33873  ordtcnvNEW  34111  xrge0iifcnv  34124  prsiga  34322  unelldsys  34349  measun  34402  measunl  34407  difelcarsg  34501  carsgclctunlem1  34508  carsggect  34509  eulerpartgbij  34563  circlemethhgt  34834  hgt750lemb  34847  bnj1416  35228  f1resfz0f1d  35349  subfacp1lem1  35414  subfacp1lem3  35417  pconnconn  35466  indispconn  35469  satfv1lem  35597  hfun  36413  onint1  36684  bj-fununsn2  37621  pibt2  37786  lindsenlbs  37989  poimirlem3  37997  poimirlem5  37999  poimirlem11  38005  poimirlem12  38006  poimirlem13  38007  poimirlem14  38008  poimirlem15  38009  poimirlem16  38010  poimirlem19  38013  poimirlem20  38014  poimirlem21  38015  poimirlem22  38016  poimirlem28  38022  poimirlem30  38024  ecuncnvepres  38769  padd02  40311  paddcom  40312  pclfinclN  40449  djhcom  41904  elrfi  43150  fzsplit1nn0  43210  eldioph2lem1  43216  eldioph2lem2  43217  diophin  43228  eldioph4b  43263  diophren  43265  kelac2  43517  pwssplit4  43541  iocunico  43663  rp-fakeuninass  43967  iunrelexp0  44153  corcltrcl  44190  frege124d  44212  mnuprdlem1  44723  equncomVD  45318  iunconnlem2  45385  snunioo1  45964  iccdifioo  45967  limciccioolb  46073  sumnnodd  46082  dirkercncflem2  46554  dirkercncflem3  46555  fourierdlem32  46589  fourierdlem93  46649  isomenndlem  46980  hoidmvlelem2  47046  hspmbllem1  47076  hspmbllem2  47077  fsumsplitsndif  47851  isubgr3stgrlem1  48464  usgrexmpl1edg  48522  usgrexmpl2edg  48527  aacllem  50298