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

Theorem uncom 4011
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 857 . . 3 ((𝑥𝐴𝑥𝐵) ↔ (𝑥𝐵𝑥𝐴))
2 elun 4007 . . 3 (𝑥 ∈ (𝐵𝐴) ↔ (𝑥𝐵𝑥𝐴))
31, 2bitr4i 270 . 2 ((𝑥𝐴𝑥𝐵) ↔ 𝑥 ∈ (𝐵𝐴))
43uneqri 4009 1 (𝐴𝐵) = (𝐵𝐴)
Colors of variables: wff setvar class
Syntax hints:  wo 834   = wceq 1508  wcel 2051  cun 3820
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1759  ax-4 1773  ax-5 1870  ax-6 1929  ax-7 1966  ax-8 2053  ax-9 2060  ax-10 2080  ax-11 2094  ax-12 2107  ax-ext 2743
This theorem depends on definitions:  df-bi 199  df-an 388  df-or 835  df-tru 1511  df-ex 1744  df-nf 1748  df-sb 2017  df-clab 2752  df-cleq 2764  df-clel 2839  df-nfc 2911  df-v 3410  df-un 3827
This theorem is referenced by:  equncom  4012  uneq2  4015  un12  4025  un23  4026  ssun2  4031  unss2  4039  ssequn2  4041  symdifcom  4101  undir  4134  unineq  4135  dif32  4148  0un  4226  disjpss  4287  undif1  4301  undif2  4302  difcom  4311  uneqdifeq  4315  dfif4  4359  dfif5  4360  prcom  4538  tpass  4558  prprc1  4571  difsnid  4613  ssunsn2  4630  sspr  4636  sstp  4637  symdifv  4870  iunxdif3  4879  unidif0  5110  difxp2  5860  suc0  6100  fununfun  6232  fresaunres2  6376  fresaunres1  6377  f1oprswap  6484  fvun2  6581  fvsnun2  6768  fvsnun2OLD  6770  fsnunfv  6774  fveqf1o  6881  difex2  7297  elpwun  7306  fnsuppeq0  7659  oev2  7948  oacomf1o  7990  ralxpmap  8256  undifixp  8293  dfdom2  8330  domunsncan  8411  enfixsn  8420  domunsn  8461  limensuci  8487  phplem2  8491  enp1ilem  8545  findcard2  8551  findcard2s  8552  frfi  8556  domunfican  8584  fsuppunbi  8647  elfiun  8687  infdifsn  8912  cantnfp1lem3  8935  rankmapu  9099  djuunxp  9142  infunsdom1  9431  infunsdom  9432  infxp  9433  ackbij1lem2  9439  ackbij1lem18  9455  fin1a2lem10  9627  fin1a2lem13  9630  zornn0g  9723  alephadd  9795  fpwwe2lem13  9860  canthp1lem1  9870  xrsupss  12516  xrinfmss  12517  supxrmnf  12524  prunioo  12681  fzsuc2  12779  fzdifsuc  12781  fseq1p1m1  12795  hashinf  13508  hashun3  13556  hashbclem  13621  relexpcnv  14253  modfsummods  15006  incexclem  15049  lcmfunsnlem  15839  ramub1lem1  16216  setsid  16392  mreexexlem3d  16787  mreexexlem4d  16788  cnvtsr  17702  gsumzaddlem  18806  gsummptfzsplitl  18818  dmdprdsplit2  18930  lspsnat  19651  lsppratlem3  19655  indistopon  21328  indistps  21338  indistps2  21339  ordtcnv  21528  leordtval2  21539  lecldbas  21546  cmpcld  21729  iunconn  21755  ufprim  22236  alexsubALTlem3  22376  ptcmplem1  22379  xpsdsval  22709  iccntr  23147  reconn  23154  volun  23864  voliunlem1  23869  icombl  23883  ioombl  23884  ismbf3d  23973  itgioo  24134  itgsplitioo  24156  lhop  24331  plyeq0  24519  fta1lem  24614  birthdaylem2  25247  lgsquadlem2  25674  usgrfilem  26827  ex-dif  27995  shjcom  28931  indifundif  30074  imadifxp  30134  difioo  30281  cycpmcl  30478  cycpm2tr  30480  lindsunlem  30681  lindsun  30682  ordtcnvNEW  30839  xrge0iifcnv  30852  prsiga  31067  unelldsys  31094  measun  31147  measunl  31152  difelcarsg  31245  carsgclctunlem1  31252  carsggect  31253  eulerpartgbij  31307  circlemethhgt  31594  hgt750lemb  31607  bnj1416  31988  subfacp1lem1  32048  subfacp1lem3  32051  pconnconn  32100  indispconn  32103  nosepdm  32746  hfun  33197  onint1  33354  bj-pr22val  33886  bj-fununsn2  34042  pibt2  34176  lindsenlbs  34365  poimirlem3  34373  poimirlem5  34375  poimirlem11  34381  poimirlem12  34382  poimirlem13  34383  poimirlem14  34384  poimirlem15  34385  poimirlem16  34386  poimirlem19  34389  poimirlem20  34390  poimirlem21  34391  poimirlem22  34392  poimirlem28  34398  poimirlem30  34400  padd02  36430  paddcom  36431  pclfinclN  36568  djhcom  38023  elrfi  38724  fzsplit1nn0  38784  eldioph2lem1  38790  eldioph2lem2  38791  diophin  38803  eldioph4b  38842  diophren  38844  kelac2  39099  pwssplit4  39123  iocunico  39251  rp-fakeuninass  39316  iunrelexp0  39448  corcltrcl  39485  frege124d  39507  mnuprdlem1  40021  equncomVD  40658  iunconnlem2  40725  snunioo1  41251  iccdifioo  41254  fsumsplit1  41316  limciccioolb  41365  sumnnodd  41374  dirkercncflem2  41852  dirkercncflem3  41853  fourierdlem32  41887  fourierdlem93  41947  isomenndlem  42275  hoidmvlelem2  42341  hspmbllem1  42371  hspmbllem2  42372  fsumsplitsndif  42971  aacllem  44301
  Copyright terms: Public domain W3C validator