Theorem uncom 3647

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 387	. . 3
2		elun 3644	. . 3
3	1, 2	bitr4i 252	. 2
4	3	uneqri 3645	1

Syntax hints:  \/wo 368  =wceq 1395  e.wcel 1818  u.cun 3473

This theorem is referenced by:  equncom  3648  uneq2  3651  un12  3661  un23  3662  ssun2  3667  unss2  3674  ssequn2  3676  undir  3746  unineq  3747  dif32  3760  disjpss  3877  undif1  3903  undif2  3904  difcom  3912  uneqdifeq  3916  dfif4  3956  dfif5  3957  prcom  4108  tpass  4128  prprc1  4140  difsnid  4176  ssunsn2  4189  sspr  4193  sstp  4194  unidif0  4625  suc0  4957  difxp2  5438  fununfun  5637  fresaunres2  5762  fresaunres1  5763  f1oprswap  5860  fvun2  5945  fvsnun2  6107  fsnunfv  6111  fnsuppeq0OLD  6132  fveqf1o  6205  difex2  6607  elpwun  6613  fnsuppeq0  6947  oev2  7192  oacomf1o  7233  ralxpmap  7488  undifixp  7525  dfdom2  7561  domunsncan  7637  enfixsn  7646  domunsn  7687  limensuci  7713  phplem2  7717  enp1ilem  7774  findcard2  7780  findcard2s  7781  frfi  7785  domunfican  7813  fsuppunbi  7870  elfiun  7910  infdifsn  8094  cantnfp1lem3  8120  cantnfp1lem3OLD  8146  rankmapu  8317  cdacomen  8582  infunsdom1  8614  infunsdom  8615  infxp  8616  ackbij1lem2  8622  ackbij1lem18  8638  fin1a2lem10  8810  fin1a2lem13  8813  zornn0g  8906  alephadd  8973  fpwwe2lem13  9041  canthp1lem1  9051  xrsupss  11529  xrinfmss  11530  supxrmnf  11538  prunioo  11678  fzsuc2  11766  fzdifsuc  11768  fseq1p1m1  11781  hashinf  12410  hashun3  12452  hashbclem  12501  modfsummods  13607  incexclem  13648  ramub1lem1  14544  setsid  14673  mreexexlem3d  15043  mreexexlem4d  15044  cnvtsr  15852  gsumzaddlem  16934  gsummptfzsplitl  16953  dmdprdsplit2  17095  lspsnat  17791  lsppratlem3  17795  indistopon  19502  indistps  19512  indistps2  19513  ordtcnv  19702  leordtval2  19713  lecldbas  19720  cmpcld  19902  iuncon  19929  ufprim  20410  alexsubALTlem3  20549  ptcmplem1  20552  xpsdsval  20884  iccntr  21326  reconn  21333  volun  21955  voliunlem1  21960  icombl  21974  ioombl  21975  ismbf3d  22061  itgioo  22222  itgsplitioo  22244  lhop  22417  plyeq0  22608  fta1lem  22703  birthdaylem2  23282  lgsquadlem2  23630  usgrafilem1  24411  constr3pthlem1  24655  ex-dif  25144  shjcom  26276  imadifxp  27458  difioo  27593  ordtcnvNEW  27902  xrge0iifcnv  27915  prsiga  28131  measun  28182  measunl  28187  eulerpartgbij  28311  subfacp1lem1  28623  subfacp1lem3  28626  pconcon  28676  indispcon  28679  nofulllem2  29463  symdifcom  29469  symdifV  29475  hfun  29835  onint1  29914  elrfi  30626  fzsplit1nn0  30687  eldioph2lem1  30693  eldioph2lem2  30694  diophin  30706  eldioph4b  30745  diophren  30747  kelac2  31011  pwssplit4  31035  iocunico  31178  snunioo1  31552  iccdifioo  31555  fsumsplit1  31573  limciccioolb  31627  sumnnodd  31636  dirkercncflem2  31886  dirkercncflem3  31887  fourierdlem32  31921  fourierdlem93  31982  fsumsplitsndif  32346  aacllem  33216  equncomVD  33668  iunconlem2  33735  bnj1416  34095  bj-pr22val  34577  padd02  35536  paddcom  35537  pclfinclN  35674  djhcom  37132  rp-fakeuninass  37741

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-v 3111  df-un 3480