MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  uncom Structured version   Visualization version   GIF version

Theorem uncom 3605
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.
StepHypRef Expression
1 orcom 396 . . 3 ((𝑥𝐴𝑥𝐵) ↔ (𝑥𝐵𝑥𝐴))
2 elun 3601 . . 3 (𝑥 ∈ (𝐵𝐴) ↔ (𝑥𝐵𝑥𝐴))
31, 2bitr4i 262 . 2 ((𝑥𝐴𝑥𝐵) ↔ 𝑥 ∈ (𝐵𝐴))
43uneqri 3603 1 (𝐴𝐵) = (𝐵𝐴)
Colors of variables: wff setvar class
Syntax hints:  wo 377   = wceq 1468  wcel 1937  cun 3424
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1698  ax-4 1711  ax-5 1789  ax-6 1836  ax-7 1883  ax-10 1965  ax-11 1970  ax-12 1983  ax-13 2137  ax-ext 2485
This theorem depends on definitions:  df-bi 192  df-or 379  df-an 380  df-tru 1471  df-ex 1693  df-nf 1697  df-sb 1829  df-clab 2492  df-cleq 2498  df-clel 2501  df-nfc 2635  df-v 3068  df-un 3431
This theorem is referenced by:  equncom  3606  uneq2  3609  un12  3619  un23  3620  ssun2  3625  unss2  3632  ssequn2  3634  symdifcom  3691  undir  3719  unineq  3720  dif32  3733  disjpss  3855  undif1  3869  undif2  3870  difcom  3879  uneqdifeq  3883  dfif4  3923  dfif5  3924  prcom  4078  tpass  4098  prprc1  4110  difsnid  4147  ssunsn2  4161  sspr  4165  sstp  4166  symdifv  4385  iunxdif3  4393  unidif0  4614  difxp2  5313  suc0  5548  fununfun  5677  fresaunres2  5813  fresaunres1  5814  f1oprswap  5916  fvun2  6004  fvsnun2  6168  fsnunfv  6172  fveqf1o  6271  difex2  6675  elpwun  6681  fnsuppeq0  7021  oev2  7302  oacomf1o  7343  ralxpmap  7604  undifixp  7641  dfdom2  7678  domunsncan  7756  enfixsn  7765  domunsn  7806  limensuci  7832  phplem2  7836  enp1ilem  7890  findcard2  7896  findcard2s  7897  frfi  7901  domunfican  7929  fsuppunbi  7989  elfiun  8029  infdifsn  8247  cantnfp1lem3  8270  rankmapu  8434  cdacomen  8696  infunsdom1  8728  infunsdom  8729  infxp  8730  ackbij1lem2  8736  ackbij1lem18  8752  fin1a2lem10  8924  fin1a2lem13  8927  zornn0g  9020  alephadd  9087  fpwwe2lem13  9152  canthp1lem1  9162  xrsupss  11689  xrinfmss  11690  supxrmnf  11698  prunioo  11857  fzsuc2  11951  fzdifsuc  11953  fseq1p1m1  11966  hashinf  12634  hashun3  12681  hashbclem  12738  relexpcnv  13258  modfsummods  14013  incexclem  14054  lcmfunsnlem  14776  ramub1lem1  15146  setsid  15329  mreexexlem3d  15717  mreexexlem4d  15718  cnvtsr  16633  gsumzaddlem  17715  gsummptfzsplitl  17727  dmdprdsplit2  17839  lspsnat  18528  lsppratlem3  18532  indistopon  20173  indistps  20183  indistps2  20184  ordtcnv  20374  leordtval2  20385  lecldbas  20392  cmpcld  20574  iuncon  20600  ufprim  21082  alexsubALTlem3  21222  ptcmplem1  21225  xpsdsval  21554  iccntr  21997  reconn  22004  volun  22658  voliunlem1  22663  icombl  22677  ioombl  22678  ismbf3d  22771  itgioo  22934  itgsplitioo  22956  lhop  23129  plyeq0  23326  fta1lem  23421  birthdaylem2  24039  lgsquadlem2  24444  usgrafilem1  25300  constr3pthlem1  25544  ex-dif  26033  shjcom  27174  indifundif  28313  imadifxp  28370  difioo  28520  ordtcnvNEW  28881  xrge0iifcnv  28894  prsiga  29108  unelldsys  29135  measun  29188  measunl  29193  difelcarsg  29296  carsgclctunlem1  29303  carsggect  29304  eulerpartgbij  29359  bnj1416  30000  subfacp1lem1  30054  subfacp1lem3  30057  pconcon  30106  indispcon  30109  nofulllem2  30743  hfun  31096  onint1  31258  bj-pr22val  31799  lindsenlbs  32173  poimirlem3  32181  poimirlem5  32183  poimirlem11  32189  poimirlem12  32190  poimirlem13  32191  poimirlem14  32192  poimirlem15  32193  poimirlem16  32194  poimirlem19  32197  poimirlem20  32198  poimirlem21  32199  poimirlem22  32200  poimirlem28  32206  poimirlem30  32208  padd02  33617  paddcom  33618  pclfinclN  33755  djhcom  35213  elrfi  35776  fzsplit1nn0  35836  eldioph2lem1  35842  eldioph2lem2  35843  diophin  35855  eldioph4b  35894  diophren  35896  kelac2  36163  pwssplit4  36187  iocunico  36335  rp-fakeuninass  36401  iunrelexp0  36533  corcltrcl  36570  frege124d  36592  equncomVD  37613  iunconlem2  37680  0un  37729  snunioo1  38013  iccdifioo  38016  fsumsplit1  38052  limciccioolb  38105  sumnnodd  38114  dirkercncflem2  38402  dirkercncflem3  38403  fourierdlem32  38438  fourierdlem93  38499  prsal  38623  isomenndlem  38815  hoidmvlelem2  38881  hspmbllem1  38911  hspmbllem2  38912  fsumsplitsndif  39620  usgrfilem  39946  aacllem  41727
  Copyright terms: Public domain W3C validator