Theorem eqcom 2740

Description: Commutative law for class equality. Theorem 6.5 of [Quine] p. 41. (Contributed by NM, 26-May-1993.) (Proof shortened by Wolf Lammen, 19-Nov-2019.)

Assertion

Ref	Expression
eqcom	⊢ (𝐴 = 𝐵 ↔ 𝐵 = 𝐴)

Proof of Theorem eqcom

Step	Hyp	Ref	Expression
1		id 22	. . 3 ⊢ (𝐴 = 𝐵 → 𝐴 = 𝐵)
2	1	eqcomd 2739	. 2 ⊢ (𝐴 = 𝐵 → 𝐵 = 𝐴)
3		id 22	. . 3 ⊢ (𝐵 = 𝐴 → 𝐵 = 𝐴)
4	3	eqcomd 2739	. 2 ⊢ (𝐵 = 𝐴 → 𝐴 = 𝐵)
5	2, 4	impbii 208	1 ⊢ (𝐴 = 𝐵 ↔ 𝐵 = 𝐴)

Syntax hints:   ↔ wb 205   = wceq 1542

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-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2725

This theorem is referenced by:  eqcoms  2741  eqcomi  2742  neqcomd  2743  eqeq2d  2744  eqtr2OLD  2758  eqtr3OLD  2760  eqabcb  2876  necom  2995  nesym  2998  pm13.181OLD  3025  gencbvex  3536  clel5  3656  eqsbc2  3847  dfss  3967  sspsstri  4103  ssnelpss  4112  ssdifim  4263  disj  4448  disj4  4459  reuprg0  4707  preq1b  4848  invdisj  5133  disjprgw  5144  disjprg  5145  dtruALT  5387  reusv3  5404  opthg2  5480  copsex2g  5494  copsex4g  5496  opcom  5502  opeqsng  5504  opeqpr  5506  snopeqop  5507  propeqop  5508  opthwiener  5515  vopelopabsb  5530  opthprc  5741  elxp3  5743  relop  5851  dmopab3  5920  rncoeq  5975  restidsing  6053  somin1  6135  xpcan  6176  xpcan2  6177  dfrel4v  6190  dmsnn0  6207  reu3op  6292  reuop  6293  opreu2reurex  6294  ordtri2  6400  ordtri2or3  6465  suc11  6472  on0eqel  6489  snsn0non  6490  iota1  6521  iotan0  6534  sniota  6535  mptfnf  6686  fresaunres1  6765  dffn5  6951  fvelrnb  6953  dfimafn2  6956  funimass4  6957  feqmptdf  6963  fnsnfv  6971  fnsnfvOLD  6972  dmfco  6988  fndmdif  7044  fneqeql  7048  rexrn  7089  ralrn  7090  elrnrexdmb  7092  dffo4  7105  funopsn  7146  ftpg  7154  fprb  7195  rexima  7239  ralima  7240  fvclss  7241  dff13  7254  f1eqcocnv  7299  f1eqcocnvOLD  7300  fnssintima  7359  imaeqsexv  7360  riotaeqimp  7392  eusvobj2  7401  f1ocnvfv3  7404  oprabidw  7440  oprabid  7441  oprabv  7469  eloprabga  7516  eloprabgaOLD  7517  ovelimab  7585  onmindif2  7795  br1steqg  7997  br2ndeqg  7998  dfoprab3  8040  opiota  8045  f1o2ndf1  8108  soseq  8145  brtpos2  8217  tpossym  8243  mpocurryd  8254  rdglim2  8432  tz7.48lem  8441  oaf1o  8563  omopthi  8660  erth2  8753  brecop  8804  erovlem  8807  ecopovsym  8813  eceqoveq  8816  xpcomco  9062  omxpenlem  9073  mapen  9141  nneneq  9209  nneneqOLD  9221  unxpdomlem3  9252  unfilem1  9310  mapfien  9403  supgtoreq  9465  wemapsolem  9545  suc11reg  9614  inf3lem2  9624  inf3lem6  9628  ttrcltr  9711  djulf1o  9907  djurf1o  9908  infenaleph  10086  isinfcard  10087  dfac5  10123  cfeq0  10251  cfsuc  10252  ssfin4  10305  fin23lem25  10319  fin23lem22  10322  fin23lem40  10346  fin1a2lem5  10399  axcclem  10452  brdom7disj  10526  brdom6disj  10527  inar1  10770  psslinpr  11026  ltexprlem4  11034  ltsrpr  11072  mulgt0sr  11100  elreal  11126  ltresr  11135  leloe  11300  eqlei2  11325  addsubeq4  11475  subcan2  11485  negcon1  11512  negcon2  11513  addid0  11633  addeq0  11637  divmul2  11876  conjmul  11931  rereccl  11932  creur  12206  creui  12207  nndiv  12258  nn0sub  12522  elnn0z  12571  elznn0  12573  xrleloe  13123  ngtmnft  13145  icoshftf1o  13451  iccf1o  13473  fzen  13518  fzneuz  13582  injresinj  13753  fleqceilz  13819  mod0  13841  modmuladdnn0  13880  modirr  13907  addmodlteq  13911  nn0ennn  13944  hashrabsn01  14333  hashsdom  14341  hashgt12el2  14383  hashbclem  14411  hashfacen  14413  hashfacenOLD  14414  hashf1lem1  14415  hashf1lem1OLD  14416  hashtpg  14446  fi1uzind  14458  ccatw2s1p1  14586  wrd2ind  14673  cshw1  14772  cshwsexa  14774  scshwfzeqfzo  14777  s2f1o  14867  wwlktovfo  14909  dmtrclfv  14965  cjreb  15070  leabs  15246  reusq0  15409  incexc2  15784  rpnnen2lem12  16168  dvdsval2  16200  dvdsabseq  16256  dvdsflip  16260  odd2np1  16284  oddm1even  16286  sqoddm1div8z  16297  m1exp1  16319  divalglem4  16339  divalglem8  16343  divalgb  16347  modremain  16351  zeqzmulgcd  16451  dfgcd2  16488  lcmfpr  16564  lcmftp  16573  lcmfunsnlem2  16577  divgcdcoprm0  16602  prm2orodd  16628  hashdvds  16708  oddprmdvds  16836  vdwlem12  16925  cshwshashlem1  17029  cshwsiun  17033  initoid  17951  termoid  17952  setcinv  18040  yonedainv  18234  joinfval  18326  joinfval2  18327  meetfval  18340  meetfval2  18341  latnle  18426  sgrp2nmndlem3  18806  grpid  18860  grpinvcnv  18891  grplmulf1o  18897  grpsubeq0  18909  grpsubadd  18911  grplactcnv  18926  isnsg4  19047  cycsubmel  19077  conjghm  19123  conjnmzb  19127  gacan  19169  gapm  19170  cntzrec  19200  oppgcntz  19231  fvcosymgeq  19297  odmulgeq  19425  dfod2  19432  sylow3lem3  19497  sylow3lem6  19500  lssnle  19542  lsmhash  19573  efgredlemb  19614  efgrelexlemb  19618  dprd2d2  19914  ablfac1eulem  19942  pgpfac1lem2  19945  pgpfac1lem4  19948  dvdsrval  20175  dvdsr02  20186  01eq0ring  20305  0ring01eqbi  20307  rmodislmodlem  20539  lvecinv  20726  rspsn  20892  prmirredlem  21042  zndvds  21105  znleval  21110  psrbagconf1o  21489  psrbagconf1oOLD  21490  mplmonmul  21591  gsummoncoe1  21828  mat1dimelbas  21973  mat1dimbas  21974  1mavmul  22050  ma1repveval  22073  mulmarep1gsum1  22075  mdetunilem9  22122  m2cpminvid2lem  22256  pmatcollpw3lem  22285  mp2pm2mplem4  22311  toponsspwpw  22424  dmtopon  22425  cmpfi  22912  ssref  23016  qtopeu  23220  hmeoimaf1o  23274  txhmeo  23307  fbasrn  23388  rnelfmlem  23456  hauspwpwf1  23491  alexsubALTlem4  23554  qustgpopn  23624  qustgphaus  23627  fmucndlem  23796  isngp3  24107  isngp4  24121  metnrmlem1a  24374  icopnfcnv  24458  iccpnfcnv  24460  ivthle  24973  ivthle2  24974  dyadmbl  25117  mbfinf  25182  i1fmulclem  25220  itg1mulc  25222  mvth  25509  dvivth  25527  lhop2  25532  dvdsq1p  25678  reeff1o  25959  coseq1  26034  recosf1o  26044  resinf1o  26045  efopn  26166  cxpeq  26265  logreclem  26267  affineequiv  26328  affineequiv4  26331  affineequivne  26332  quad2  26344  dcubic  26351  mcubic  26352  quart  26366  atandm2  26382  rlimcnp2  26471  amgm  26495  wilthlem2  26573  mumullem2  26684  sqff1o  26686  dvdsflf1o  26691  gausslemma2dlem0i  26867  lgseisenlem2  26879  lgsquadlem2  26884  2lgslem1c  26896  2lgsoddprmlem2  26912  2lgsoddprm  26919  2sq2  26936  addsq2reu  26943  2sqreultlem  26950  2sqreunnltlem  26953  2sqreulem3  26956  sltval2  27159  sltintdifex  27164  sltres  27165  nosepon  27168  noextenddif  27171  nosepssdm  27189  nogt01o  27199  nosupprefixmo  27203  noinfprefixmo  27204  nosupno  27206  noinfno  27221  sleloe  27257  eqscut2  27308  scutbdaylt  27320  elold  27365  made0  27369  lrrecfr  27429  subadds  27541  tgjustf  27755  legtrid  27873  legso  27881  islmib  28069  lmicom  28070  lmiinv  28074  lmimid  28076  lmiopp  28084  colinearalglem2  28196  colinearalg  28199  ax5seglem4  28221  ax5seglem5  28222  axlowdimlem13  28243  axeuclidlem  28251  axeuclid  28252  axcontlem2  28254  axcontlem4  28256  elntg2  28274  structiedg0val  28313  usgredgsscusgredg  28747  fusgrn0degnn0  28787  umgr2v2evtxel  28810  vdiscusgrb  28818  uspgr2wlkeq  28934  wlk0prc  28942  wlklenvclwlk  28943  wlkp1lem8  28968  spthdep  29022  usgr2pthlem  29051  usgr2pth  29052  wlkiswwlksupgr2  29162  wlklnwwlkln2lem  29167  wwlksnextproplem3  29196  umgr2adedgwlk  29230  umgr2adedgspth  29233  umgr2wlkon  29235  umgrwwlks2on  29242  elwwlks2  29251  elwspths2spth  29252  clwlkclwwlklem2a4  29281  clwlkclwwlklem2  29284  erclwwlkref  29304  clwwlkf  29331  erclwwlknref  29353  erclwwlknsym  29354  erclwwlkntr  29355  hashecclwwlkn1  29361  umgrhashecclwwlk  29362  eupth2lem2  29503  eucrct2eupth  29529  numclwwlkqhash  29659  isgrpo  29781  hvsubaddi  30350  hire  30378  shmodsi  30673  omlsilem  30686  chcon1i  30749  chnlei  30769  pjoml3i  30870  cmbr2i  30880  chscllem2  30922  adjsym  31117  eigorthi  31121  dfadj2  31169  adjval2  31175  cnvadj  31176  dmadjrnb  31190  adjvalval  31221  cnlnadjeui  31361  cnlnssadj  31364  adjbdln  31367  pjimai  31460  pjin2i  31477  pjin3i  31478  stadd3i  31532  largei  31551  cvnbtwn3  31572  cvnbtwn4  31573  mddmd2  31593  superpos  31638  atnemeq0  31661  sumdmdii  31699  sumdmdlem  31702  addltmulALT  31730  opreu2reuALT  31748  foresf1o  31773  difeq  31787  disjrdx  31853  fcoinvbr  31867  fmptco1f1o  31888  dfimafnf  31891  funcnvmpt  31923  curry2ima  31961  intimafv  31963  cnvoprabOLD  31976  elicoelioo  32020  wrdt2ind  32148  swrdrn3  32150  orngsqr  32453  qusker  32495  eqg0el  32504  dvdsrspss  32522  lsmsnorb  32532  zarcls  32885  xrmulc1cn  32941  xrge0iifcnv  32944  ind1a  33048  esumfsup  33099  esumpcvgval  33107  esumcvg  33115  esum2dlem  33121  issgon  33152  eulerpartgbij  33402  eulerpartlemgh  33408  ballotlemsima  33545  bnj1366  33871  bnj553  33940  bnj964  33985  cusgredgex  34143  revwlk  34146  loop1cycl  34159  subfacp1lem3  34204  subfacp1lem5  34206  erdszelem9  34221  prv1n  34453  quad3  34686  br6  34758  elintfv  34767  dfon2lem5  34790  dfon2lem8  34793  brbigcup  34901  dfbigcup2  34902  elfix  34906  ellimits  34913  snelsingles  34925  dfiota3  34926  imageval  34933  brapply  34941  brsuccf  34944  funpartlem  34945  brfullfun  34951  dfrecs2  34953  dfrdg4  34954  altopthbg  34971  altopthc  34974  altopthd  34975  altopelaltxp  34979  brsegle  35111  outsideofrflx  35130  elicc3  35250  nn0prpw  35256  opnregcld  35263  cldregopn  35264  fneval  35285  topfneec  35288  knoppndvlem9  35444  bj-elgab  35867  bj-gabima  35868  bj-elsngl  35897  bj-snglc  35898  bj-projval  35925  bj-disj2r  35957  bj-restreg  36028  bj-0int  36030  copsex2b  36069  bj-inftyexpitaudisj  36134  bj-inftyexpidisj  36139  bj-bary1lem1  36240  topdifinffinlem  36276  topdifinfeq  36279  fvineqsnf1  36339  curf  36514  uncf  36515  curunc  36518  unccur  36519  poimirlem2  36538  poimirlem16  36552  poimirlem17  36553  poimirlem19  36555  poimirlem20  36556  poimirlem27  36563  mblfinlem2  36574  mbfresfi  36582  itg2addnclem2  36588  ftc1anclem3  36611  fdc  36661  heibor1  36726  opidonOLD  36768  0rngo  36943  smprngopr  36968  isfldidl  36984  isfldidl2  36985  eqbrb  37147  eqelb  37149  ideq2  37224  relcnveq  37239  n0elqs  37243  disjressuc2  37306  elrelscnveq  37410  disjdmqscossss  37721  lcvnbtwn3  37946  lcvexchlem1  37952  lsatnem0  37963  opcon1b  38116  omllaw2N  38162  cmtbr2N  38171  leatb  38210  cvlsupr2  38261  glbconxN  38297  islln3  38429  llnexatN  38440  islpln3  38452  lplnexatN  38482  islvol3  38495  dalem-cly  38590  isline4N  38696  2llnma3r  38707  poml4N  38872  4atex2  38996  4atex2-0bOLDN  38998  cdlemefrs29bpre0  39315  cdlemftr3  39484  cdlemb3  39525  cdlemg17h  39587  cdlemg17pq  39591  cdlemg19  39603  cdlemg21  39605  tendoex  39894  dva1dim  39904  dihglb2  40261  doch11  40292  dochsordN  40293  lcfrlem9  40469  hlhillcs  40881  lcmineqlem4  40945  metakunt1  41033  metakunt6  41038  metakunt15  41047  metakunt16  41048  fsuppind  41210  addsubeq4com  41240  elrfirn  41481  isnacs2  41492  isnacs3  41496  fiphp3d  41605  wopprc  41817  islnm2  41868  kercvrlsm  41873  fgraphopab  42000  tfsconcatlem  42134  tfsconcatrn  42140  tfsconcat0i  42143  tfsconcat0b  42144  tfsconcatrev  42146  oaun3lem1  42172  oadif1lem  42177  oadif1  42178  rp-fakeuninass  42315  snen1g  42323  iscard4  42332  sqrtcval  42440  frege124d  42560  frege129d  42562  frege92  42754  dffrege99  42761  clsk3nimkb  42839  clsk1indlem4  42843  clsk1indlem1  42844  ntrclsiso  42866  ntrclsk3  42869  ntrclsk13  42870  ntrneik4w  42899  extoimad  42964  int-sqdefd  42981  int-sqgeq0d  42986  radcnvrat  43121  bcc0  43147  opelopab4  43360  eqsbc2VD  43649  fzisoeu  44058  iuneqfzuz  44093  supxrleubrnmptf  44209  rexanuz2nf  44251  fsummulc1f  44335  fsumiunss  44339  fmul01lt1lem2  44349  sumnnodd  44394  fnlimfvre2  44441  limsupreuz  44501  limsupvaluz2  44502  liminfvalxr  44547  icccncfext  44651  cncfiooicc  44658  cncfioobdlem  44660  dvmptmulf  44701  dvmptfprodlem  44708  volioc  44736  itgioocnicc  44741  fourierdlem12  44883  fourierdlem20  44891  fourierdlem25  44896  fourierdlem33  44904  fourierdlem42  44913  fourierdlem52  44922  fourierdlem54  44924  fourierdlem57  44927  fourierdlem58  44928  fourierdlem59  44929  fourierdlem63  44933  fourierdlem65  44935  fourierdlem68  44938  fourierdlem73  44943  fourierdlem74  44944  fourierdlem75  44945  fourierdlem80  44950  fourierdlem81  44951  rrndistlt  45054  sge0ltfirpmpt2  45190  sge0pnfmpt  45209  hoidmv1le  45358  hoidmvle  45364  vonioolem2  45445  smflimlem3  45537  euabsneu  45786  funressnfv  45801  aiotaval  45851  reuf1odnf  45863  reuf1od  45864  afvpcfv0  45902  dfafn5a  45916  afvelrnb  45919  afvelrnb0  45920  dfaimafn2  45922  dfatsnafv2  46008  dfatdmfcoafv2  46010  f1oresf1o2  46047  0nelsetpreimafv  46106  fargshiftfo  46158  sprsymrelf1  46212  reupr  46238  fmtnorec2lem  46258  fmtnoprmfac1  46281  fmtnoprmfac2  46283  sfprmdvdsmersenne  46319  lighneallem2  46322  dfeven2  46365  dfodd3  46366  odd2np1ALTV  46390  even3prm2  46435  fppr2odd  46447  nnsum3primesgbe  46508  nnsum3primesle9  46510  isomuspgrlem2d  46547  0nodd  46628  2nodd  46630  lmod0rng  46690  rngqiprngimf1lem  46827  rngcinv  46927  rngcinvALTV  46939  ringcinv  46978  ringcinvALTV  47002  lcoel0  47157  lindslinindimp2lem4  47190  ldepspr  47202  lincresunit3  47210  nn0sumshdiglemB  47354  nn0sumshdiglem1  47355  rrx2pnedifcoorneorr  47451  eenglngeehlnmlem1  47471  eenglngeehlnmlem2  47472  rrx2linest  47476  rrx2linest2  47478  rrxsphere  47482  line2ylem  47485  line2x  47488  itscnhlc0xyqsol  47499  itschlc0xyqsol1  47500  itsclinecirc0b  47508  2itscp  47515  inlinecirc02plem  47520