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  27307  scutbdaylt  27319  elold  27364  made0  27368  lrrecfr  27427  subadds  27538  tgjustf  27724  legtrid  27842  legso  27850  islmib  28038  lmicom  28039  lmiinv  28043  lmimid  28045  lmiopp  28053  colinearalglem2  28165  colinearalg  28168  ax5seglem4  28190  ax5seglem5  28191  axlowdimlem13  28212  axeuclidlem  28220  axeuclid  28221  axcontlem2  28223  axcontlem4  28225  elntg2  28243  structiedg0val  28282  usgredgsscusgredg  28716  fusgrn0degnn0  28756  umgr2v2evtxel  28779  vdiscusgrb  28787  uspgr2wlkeq  28903  wlk0prc  28911  wlklenvclwlk  28912  wlkp1lem8  28937  spthdep  28991  usgr2pthlem  29020  usgr2pth  29021  wlkiswwlksupgr2  29131  wlklnwwlkln2lem  29136  wwlksnextproplem3  29165  umgr2adedgwlk  29199  umgr2adedgspth  29202  umgr2wlkon  29204  umgrwwlks2on  29211  elwwlks2  29220  elwspths2spth  29221  clwlkclwwlklem2a4  29250  clwlkclwwlklem2  29253  erclwwlkref  29273  clwwlkf  29300  erclwwlknref  29322  erclwwlknsym  29323  erclwwlkntr  29324  hashecclwwlkn1  29330  umgrhashecclwwlk  29331  eupth2lem2  29472  eucrct2eupth  29498  numclwwlkqhash  29628  isgrpo  29750  hvsubaddi  30319  hire  30347  shmodsi  30642  omlsilem  30655  chcon1i  30718  chnlei  30738  pjoml3i  30839  cmbr2i  30849  chscllem2  30891  adjsym  31086  eigorthi  31090  dfadj2  31138  adjval2  31144  cnvadj  31145  dmadjrnb  31159  adjvalval  31190  cnlnadjeui  31330  cnlnssadj  31333  adjbdln  31336  pjimai  31429  pjin2i  31446  pjin3i  31447  stadd3i  31501  largei  31520  cvnbtwn3  31541  cvnbtwn4  31542  mddmd2  31562  superpos  31607  atnemeq0  31630  sumdmdii  31668  sumdmdlem  31671  addltmulALT  31699  opreu2reuALT  31717  foresf1o  31742  difeq  31756  disjrdx  31822  fcoinvbr  31836  fmptco1f1o  31857  dfimafnf  31860  funcnvmpt  31892  curry2ima  31930  intimafv  31932  cnvoprabOLD  31945  elicoelioo  31989  wrdt2ind  32117  swrdrn3  32119  orngsqr  32422  qusker  32464  eqg0el  32473  dvdsrspss  32491  lsmsnorb  32501  zarcls  32854  xrmulc1cn  32910  xrge0iifcnv  32913  ind1a  33017  esumfsup  33068  esumpcvgval  33076  esumcvg  33084  esum2dlem  33090  issgon  33121  eulerpartgbij  33371  eulerpartlemgh  33377  ballotlemsima  33514  bnj1366  33840  bnj553  33909  bnj964  33954  cusgredgex  34112  revwlk  34115  loop1cycl  34128  subfacp1lem3  34173  subfacp1lem5  34175  erdszelem9  34190  prv1n  34422  quad3  34655  br6  34727  elintfv  34736  dfon2lem5  34759  dfon2lem8  34762  brbigcup  34870  dfbigcup2  34871  elfix  34875  ellimits  34882  snelsingles  34894  dfiota3  34895  imageval  34902  brapply  34910  brsuccf  34913  funpartlem  34914  brfullfun  34920  dfrecs2  34922  dfrdg4  34923  altopthbg  34940  altopthc  34943  altopthd  34944  altopelaltxp  34948  brsegle  35080  outsideofrflx  35099  elicc3  35202  nn0prpw  35208  opnregcld  35215  cldregopn  35216  fneval  35237  topfneec  35240  knoppndvlem9  35396  bj-elgab  35819  bj-gabima  35820  bj-elsngl  35849  bj-snglc  35850  bj-projval  35877  bj-disj2r  35909  bj-restreg  35980  bj-0int  35982  copsex2b  36021  bj-inftyexpitaudisj  36086  bj-inftyexpidisj  36091  bj-bary1lem1  36192  topdifinffinlem  36228  topdifinfeq  36231  fvineqsnf1  36291  curf  36466  uncf  36467  curunc  36470  unccur  36471  poimirlem2  36490  poimirlem16  36504  poimirlem17  36505  poimirlem19  36507  poimirlem20  36508  poimirlem27  36515  mblfinlem2  36526  mbfresfi  36534  itg2addnclem2  36540  ftc1anclem3  36563  fdc  36613  heibor1  36678  opidonOLD  36720  0rngo  36895  smprngopr  36920  isfldidl  36936  isfldidl2  36937  eqbrb  37099  eqelb  37101  ideq2  37176  relcnveq  37191  n0elqs  37195  disjressuc2  37258  elrelscnveq  37362  disjdmqscossss  37673  lcvnbtwn3  37898  lcvexchlem1  37904  lsatnem0  37915  opcon1b  38068  omllaw2N  38114  cmtbr2N  38123  leatb  38162  cvlsupr2  38213  glbconxN  38249  islln3  38381  llnexatN  38392  islpln3  38404  lplnexatN  38434  islvol3  38447  dalem-cly  38542  isline4N  38648  2llnma3r  38659  poml4N  38824  4atex2  38948  4atex2-0bOLDN  38950  cdlemefrs29bpre0  39267  cdlemftr3  39436  cdlemb3  39477  cdlemg17h  39539  cdlemg17pq  39543  cdlemg19  39555  cdlemg21  39557  tendoex  39846  dva1dim  39856  dihglb2  40213  doch11  40244  dochsordN  40245  lcfrlem9  40421  hlhillcs  40833  lcmineqlem4  40897  metakunt1  40985  metakunt6  40990  metakunt15  40999  metakunt16  41000  fsuppind  41162  addsubeq4com  41192  elrfirn  41433  isnacs2  41444  isnacs3  41448  fiphp3d  41557  wopprc  41769  islnm2  41820  kercvrlsm  41825  fgraphopab  41952  tfsconcatlem  42086  tfsconcatrn  42092  tfsconcat0i  42095  tfsconcat0b  42096  tfsconcatrev  42098  oaun3lem1  42124  oadif1lem  42129  oadif1  42130  rp-fakeuninass  42267  snen1g  42275  iscard4  42284  sqrtcval  42392  frege124d  42512  frege129d  42514  frege92  42706  dffrege99  42713  clsk3nimkb  42791  clsk1indlem4  42795  clsk1indlem1  42796  ntrclsiso  42818  ntrclsk3  42821  ntrclsk13  42822  ntrneik4w  42851  extoimad  42916  int-sqdefd  42933  int-sqgeq0d  42938  radcnvrat  43073  bcc0  43099  opelopab4  43312  eqsbc2VD  43601  fzisoeu  44010  iuneqfzuz  44045  supxrleubrnmptf  44161  rexanuz2nf  44203  fsummulc1f  44287  fsumiunss  44291  fmul01lt1lem2  44301  sumnnodd  44346  fnlimfvre2  44393  limsupreuz  44453  limsupvaluz2  44454  liminfvalxr  44499  icccncfext  44603  cncfiooicc  44610  cncfioobdlem  44612  dvmptmulf  44653  dvmptfprodlem  44660  volioc  44688  itgioocnicc  44693  fourierdlem12  44835  fourierdlem20  44843  fourierdlem25  44848  fourierdlem33  44856  fourierdlem42  44865  fourierdlem52  44874  fourierdlem54  44876  fourierdlem57  44879  fourierdlem58  44880  fourierdlem59  44881  fourierdlem63  44885  fourierdlem65  44887  fourierdlem68  44890  fourierdlem73  44895  fourierdlem74  44896  fourierdlem75  44897  fourierdlem80  44902  fourierdlem81  44903  rrndistlt  45006  sge0ltfirpmpt2  45142  sge0pnfmpt  45161  hoidmv1le  45310  hoidmvle  45316  vonioolem2  45397  smflimlem3  45489  euabsneu  45738  funressnfv  45753  aiotaval  45803  reuf1odnf  45815  reuf1od  45816  afvpcfv0  45854  dfafn5a  45868  afvelrnb  45871  afvelrnb0  45872  dfaimafn2  45874  dfatsnafv2  45960  dfatdmfcoafv2  45962  f1oresf1o2  45999  0nelsetpreimafv  46058  fargshiftfo  46110  sprsymrelf1  46164  reupr  46190  fmtnorec2lem  46210  fmtnoprmfac1  46233  fmtnoprmfac2  46235  sfprmdvdsmersenne  46271  lighneallem2  46274  dfeven2  46317  dfodd3  46318  odd2np1ALTV  46342  even3prm2  46387  fppr2odd  46399  nnsum3primesgbe  46460  nnsum3primesle9  46462  isomuspgrlem2d  46499  0nodd  46580  2nodd  46582  lmod0rng  46642  rngqiprngimf1lem  46779  rngcinv  46879  rngcinvALTV  46891  ringcinv  46930  ringcinvALTV  46954  lcoel0  47109  lindslinindimp2lem4  47142  ldepspr  47154  lincresunit3  47162  nn0sumshdiglemB  47306  nn0sumshdiglem1  47307  rrx2pnedifcoorneorr  47403  eenglngeehlnmlem1  47423  eenglngeehlnmlem2  47424  rrx2linest  47428  rrx2linest2  47430  rrxsphere  47434  line2ylem  47437  line2x  47440  itscnhlc0xyqsol  47451  itschlc0xyqsol1  47452  itsclinecirc0b  47460  2itscp  47467  inlinecirc02plem  47472