Theorem eqcom 2765

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 2764	. 2 ⊢ (𝐴 = 𝐵 → 𝐵 = 𝐴)
3		id 22	. . 3 ⊢ (𝐵 = 𝐴 → 𝐵 = 𝐴)
4	3	eqcomd 2764	. 2 ⊢ (𝐵 = 𝐴 → 𝐴 = 𝐵)
5	2, 4	impbii 212	1 ⊢ (𝐴 = 𝐵 ↔ 𝐵 = 𝐴)

Syntax hints:   ↔ wb 209   = wceq 1538

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-9 2121  ax-ext 2729

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2750

This theorem is referenced by:  eqcoms  2766  eqcomi  2767  neqcomd  2768  eqeq2d  2769  eqtr2  2779  eqtr3  2780  abeq1  2885  necom  3004  nesym  3007  pm13.181  3033  gencbvex  3466  clel5  3578  eqsbc3r  3761  dfss  3876  sspsstri  4008  ssnelpss  4017  ssdifim  4167  disj  4344  disj4  4355  reuprg0  4595  preq1b  4734  invdisj  5016  disjprgw  5027  disjprg  5028  dtruALT  5257  reusv3  5274  dtruALT2  5304  opthg2  5339  copsex2g  5352  copsex4g  5354  opcom  5360  opeqsng  5362  opeqpr  5364  snopeqop  5365  propeqop  5366  opthwiener  5373  vopelopabsb  5386  opthprc  5585  elxp3  5587  relop  5690  dmopab3  5759  rncoeq  5816  restidsing  5894  somin1  5965  xpcan  6005  xpcan2  6006  dfrel4v  6019  dmsnn0  6036  reu3op  6121  reuop  6122  opreu2reurex  6123  ordtri2  6204  ordtri2or3  6266  suc11  6272  on0eqel  6287  snsn0non  6288  iota1  6312  iotan0  6325  sniota  6326  mptfnf  6466  fresaunres1  6536  dffn5  6712  fvelrnb  6714  dfimafn2  6717  funimass4  6718  feqmptdf  6723  fnsnfv  6731  fnsnfvOLD  6732  dmfco  6748  fndmdif  6803  fneqeql  6807  rexrn  6844  ralrn  6845  elrnrexdmb  6847  dffo4  6860  funopsn  6901  ftpg  6909  fprb  6947  rexima  6991  ralima  6992  fvclss  6993  dff13  7005  f1eqcocnv  7049  f1eqcocnvOLD  7050  riotaeqimp  7134  eusvobj2  7143  f1ocnvfv3  7146  oprabidw  7181  oprabid  7182  oprabv  7208  eloprabga  7255  ovelimab  7322  onmindif2  7526  br1steqg  7715  br2ndeqg  7716  dfoprab3  7756  opiota  7761  f1o2ndf1  7823  brtpos2  7908  tpossym  7934  mpocurryd  7945  rdglim2  8078  tz7.48lem  8087  oaf1o  8199  omopthi  8294  erth2  8349  brecop  8400  erovlem  8403  ecopovsym  8409  eceqoveq  8412  xpcomco  8628  omxpenlem  8639  mapen  8703  nneneq  8722  unxpdomlem3  8762  unfilem1  8815  mapfien  8905  supgtoreq  8967  wemapsolem  9047  suc11reg  9115  inf3lem2  9125  inf3lem6  9129  djulf1o  9374  djurf1o  9375  infenaleph  9551  isinfcard  9552  dfac5  9588  cfeq0  9716  cfsuc  9717  ssfin4  9770  fin23lem25  9784  fin23lem22  9787  fin23lem40  9811  fin1a2lem5  9864  axcclem  9917  brdom7disj  9991  brdom6disj  9992  inar1  10235  psslinpr  10491  ltexprlem4  10499  ltsrpr  10537  mulgt0sr  10565  elreal  10591  ltresr  10600  leloe  10765  eqlei2  10789  addsubeq4  10939  subcan2  10949  negcon1  10976  negcon2  10977  addid0  11097  addeq0  11101  divmul2  11340  conjmul  11395  rereccl  11396  creur  11668  creui  11669  nndiv  11720  nn0sub  11984  elnn0z  12033  elznn0  12035  xrleloe  12578  ngtmnft  12600  icoshftf1o  12906  iccf1o  12928  fzen  12973  fzneuz  13037  injresinj  13207  fleqceilz  13271  mod0  13293  modmuladdnn0  13332  modirr  13359  addmodlteq  13363  nn0ennn  13396  hashrabsn01  13784  hashsdom  13792  hashgt12el2  13834  hashbclem  13860  hashfacen  13862  hashfacenOLD  13863  hashf1lem1  13864  hashf1lem1OLD  13865  hashtpg  13895  fi1uzind  13907  ccatw2s1p1  14042  ccatw2s1p1OLD  14043  wrd2ind  14132  cshw1  14231  scshwfzeqfzo  14235  s2f1o  14325  wwlktovfo  14369  dmtrclfv  14425  cjreb  14530  leabs  14707  reusq0  14870  incexc2  15241  pwm1geoserOLD  15273  rpnnen2lem12  15626  dvdsval2  15658  dvdsabseq  15714  dvdsflip  15718  odd2np1  15742  oddm1even  15744  sqoddm1div8z  15755  m1exp1  15777  divalglem4  15797  divalglem8  15801  divalgb  15805  modremain  15809  zeqzmulgcd  15909  dfgcd2  15945  lcmfpr  16023  lcmftp  16032  lcmfunsnlem2  16036  divgcdcoprm0  16061  prm2orodd  16087  hashdvds  16167  oddprmdvds  16294  vdwlem12  16383  cshwshashlem1  16487  cshwsiun  16491  initoid  17327  termoid  17328  setcinv  17416  yonedainv  17597  joinfval  17677  joinfval2  17678  meetfval  17691  meetfval2  17692  latnle  17761  sgrp2nmndlem3  18156  grpid  18206  grpinvcnv  18234  grplmulf1o  18240  grpsubeq0  18252  grpsubadd  18254  grplactcnv  18269  isnsg4  18386  cycsubmel  18410  conjghm  18456  conjnmzb  18460  gacan  18502  gapm  18503  cntzrec  18531  oppgcntz  18559  fvcosymgeq  18624  odmulgeq  18751  dfod2  18758  sylow3lem3  18821  sylow3lem6  18824  lssnle  18867  lsmhash  18898  efgredlemb  18939  efgrelexlemb  18943  dprd2d2  19234  ablfac1eulem  19262  pgpfac1lem2  19265  pgpfac1lem4  19268  dvdsrval  19466  dvdsr02  19477  rmodislmodlem  19769  lvecinv  19953  rspsn  20095  0ring01eqbi  20114  prmirredlem  20262  zndvds  20317  znleval  20322  psrbagconf1o  20698  psrbagconf1oOLD  20699  mplmonmul  20796  gsummoncoe1  21028  mat1dimelbas  21171  mat1dimbas  21172  1mavmul  21248  ma1repveval  21271  mulmarep1gsum1  21273  mdetunilem9  21320  m2cpminvid2lem  21454  pmatcollpw3lem  21483  mp2pm2mplem4  21509  toponsspwpw  21622  dmtopon  21623  cmpfi  22108  ssref  22212  qtopeu  22416  hmeoimaf1o  22470  txhmeo  22503  fbasrn  22584  rnelfmlem  22652  hauspwpwf1  22687  alexsubALTlem4  22750  qustgpopn  22820  qustgphaus  22823  fmucndlem  22992  isngp3  23300  isngp4  23314  metnrmlem1a  23559  icopnfcnv  23643  iccpnfcnv  23645  ivthle  24156  ivthle2  24157  dyadmbl  24300  mbfinf  24365  i1fmulclem  24402  itg1mulc  24404  mvth  24691  dvivth  24709  lhop2  24714  dvdsq1p  24860  reeff1o  25141  coseq1  25216  recosf1o  25226  resinf1o  25227  efopn  25348  cxpeq  25445  logreclem  25447  affineequiv  25508  affineequiv4  25511  affineequivne  25512  quad2  25524  dcubic  25531  mcubic  25532  quart  25546  atandm2  25562  rlimcnp2  25651  amgm  25675  wilthlem2  25753  mumullem2  25864  sqff1o  25866  dvdsflf1o  25871  gausslemma2dlem0i  26047  lgseisenlem2  26059  lgsquadlem2  26064  2lgslem1c  26076  2lgsoddprmlem2  26092  2lgsoddprm  26099  2sq2  26116  addsq2reu  26123  2sqreultlem  26130  2sqreunnltlem  26133  2sqreulem3  26136  tgjustf  26366  legtrid  26484  legso  26492  islmib  26680  lmicom  26681  lmiinv  26685  lmimid  26687  lmiopp  26695  colinearalglem2  26800  colinearalg  26803  ax5seglem4  26825  ax5seglem5  26826  axlowdimlem13  26847  axeuclidlem  26855  axeuclid  26856  axcontlem2  26858  axcontlem4  26860  elntg2  26878  structiedg0val  26914  usgredgsscusgredg  27348  fusgrn0degnn0  27388  umgr2v2evtxel  27411  vdiscusgrb  27419  uspgr2wlkeq  27534  wlk0prc  27542  wlklenvclwlk  27543  wlklenvclwlkOLD  27544  wlkp1lem8  27569  spthdep  27622  usgr2pthlem  27651  usgr2pth  27652  wlkiswwlksupgr2  27762  wlklnwwlkln2lem  27767  wwlksnextproplem3  27796  umgr2adedgwlk  27830  umgr2adedgspth  27833  umgr2wlkon  27835  umgrwwlks2on  27842  elwwlks2  27851  elwspths2spth  27852  clwlkclwwlklem2a4  27881  clwlkclwwlklem2  27884  erclwwlkref  27904  clwwlkf  27931  erclwwlknref  27953  erclwwlknsym  27954  erclwwlkntr  27955  hashecclwwlkn1  27961  umgrhashecclwwlk  27962  eupth2lem2  28103  eucrct2eupth  28129  numclwwlkqhash  28259  isgrpo  28379  hvsubaddi  28948  hire  28976  shmodsi  29271  omlsilem  29284  chcon1i  29347  chnlei  29367  pjoml3i  29468  cmbr2i  29478  chscllem2  29520  adjsym  29715  eigorthi  29719  dfadj2  29767  adjval2  29773  cnvadj  29774  dmadjrnb  29788  adjvalval  29819  cnlnadjeui  29959  cnlnssadj  29962  adjbdln  29965  pjimai  30058  pjin2i  30075  pjin3i  30076  stadd3i  30130  largei  30149  cvnbtwn3  30170  cvnbtwn4  30171  mddmd2  30191  superpos  30236  atnemeq0  30259  sumdmdii  30297  sumdmdlem  30300  addltmulALT  30328  opreu2reuALT  30346  foresf1o  30372  difeq  30387  disjrdx  30452  fcoinvbr  30469  fmptco1f1o  30490  dfimafnf  30493  funcnvmpt  30528  curry2ima  30565  intimafv  30567  cnvoprabOLD  30579  elicoelioo  30623  wrdt2ind  30749  swrdrn3  30751  orngsqr  31029  qusker  31070  eqg0el  31078  lsmsnorb  31100  zarcls  31345  xrmulc1cn  31401  xrge0iifcnv  31404  ind1a  31506  esumfsup  31557  esumpcvgval  31565  esumcvg  31573  esum2dlem  31579  issgon  31610  eulerpartgbij  31858  eulerpartlemgh  31864  ballotlemsima  32001  bnj1366  32329  bnj553  32398  bnj964  32443  cusgredgex  32599  revwlk  32602  loop1cycl  32615  subfacp1lem3  32660  subfacp1lem5  32662  erdszelem9  32677  prv1n  32909  quad3  33144  fnssintima  33194  br6  33240  elintfv  33254  dfon2lem5  33279  dfon2lem8  33282  soseq  33358  sltval2  33444  sltintdifex  33449  sltres  33450  nosepon  33453  noextenddif  33456  nosepssdm  33474  nogt01o  33484  nosupprefixmo  33488  noinfprefixmo  33489  nosupno  33491  noinfno  33506  sleloe  33542  eqscut2  33583  scutbdaylt  33595  elold  33631  made0  33636  lrrecfr  33670  brbigcup  33771  dfbigcup2  33772  elfix  33776  ellimits  33783  snelsingles  33795  dfiota3  33796  imageval  33803  brapply  33811  brsuccf  33814  funpartlem  33815  brfullfun  33821  dfrecs2  33823  dfrdg4  33824  altopthbg  33841  altopthc  33844  altopthd  33845  altopelaltxp  33849  brsegle  33981  outsideofrflx  34000  elicc3  34077  nn0prpw  34083  opnregcld  34090  cldregopn  34091  fneval  34112  topfneec  34115  knoppndvlem9  34271  bj-elsngl  34707  bj-snglc  34708  bj-projval  34735  bj-disj2r  34767  bj-restreg  34816  bj-0int  34818  copsex2b  34857  bj-inftyexpitaudisj  34922  bj-inftyexpidisj  34927  bj-isrvec  35010  bj-bary1lem1  35027  topdifinffinlem  35066  topdifinfeq  35069  fvineqsnf1  35129  curf  35337  uncf  35338  curunc  35341  unccur  35342  poimirlem2  35361  poimirlem16  35375  poimirlem17  35376  poimirlem19  35378  poimirlem20  35379  poimirlem27  35386  mblfinlem2  35397  mbfresfi  35405  itg2addnclem2  35411  ftc1anclem3  35434  fdc  35485  heibor1  35550  opidonOLD  35592  0rngo  35767  smprngopr  35792  isfldidl  35808  isfldidl2  35809  eqelb  35964  ideq2  36027  relcnveq  36041  n0elqs  36045  elrelscnveq  36194  lcvnbtwn3  36626  lcvexchlem1  36632  lsatnem0  36643  opcon1b  36796  omllaw2N  36842  cmtbr2N  36851  leatb  36890  cvlsupr2  36941  glbconxN  36976  islln3  37108  llnexatN  37119  islpln3  37131  lplnexatN  37161  islvol3  37174  dalem-cly  37269  isline4N  37375  2llnma3r  37386  poml4N  37551  4atex2  37675  4atex2-0bOLDN  37677  cdlemefrs29bpre0  37994  cdlemftr3  38163  cdlemb3  38204  cdlemg17h  38266  cdlemg17pq  38270  cdlemg19  38282  cdlemg21  38284  tendoex  38573  dva1dim  38583  dihglb2  38940  doch11  38971  dochsordN  38972  lcfrlem9  39148  hlhillcs  39556  lcmineqlem4  39621  metakunt1  39669  metakunt6  39674  metakunt15  39683  metakunt16  39684  fsuppind  39806  addsubeq4com  39832  elrfirn  40031  isnacs2  40042  isnacs3  40046  fiphp3d  40155  wopprc  40366  islnm2  40417  kercvrlsm  40422  fgraphopab  40549  rp-fakeuninass  40619  snen1g  40627  iscard4  40636  sqrtcval  40736  frege124d  40857  frege129d  40859  frege92  41051  dffrege99  41058  clsk3nimkb  41138  clsk1indlem4  41142  clsk1indlem1  41143  ntrclsiso  41165  ntrclsk3  41168  ntrclsk13  41169  ntrneik4w  41198  extoimad  41263  int-sqdefd  41282  int-sqgeq0d  41287  radcnvrat  41413  bcc0  41439  opelopab4  41652  eqsbc3rVD  41941  fzisoeu  42322  iuneqfzuz  42357  supxrleubrnmptf  42478  fsummulc1f  42600  fsumiunss  42605  fmul01lt1lem2  42615  sumnnodd  42660  fnlimfvre2  42707  limsupreuz  42767  limsupvaluz2  42768  liminfvalxr  42813  icccncfext  42917  cncfiooicc  42924  cncfioobdlem  42926  dvmptmulf  42967  dvmptfprodlem  42974  volioc  43002  itgioocnicc  43007  fourierdlem12  43149  fourierdlem20  43157  fourierdlem25  43162  fourierdlem33  43170  fourierdlem42  43179  fourierdlem52  43188  fourierdlem54  43190  fourierdlem57  43193  fourierdlem58  43194  fourierdlem59  43195  fourierdlem63  43199  fourierdlem65  43201  fourierdlem68  43204  fourierdlem73  43209  fourierdlem74  43210  fourierdlem75  43211  fourierdlem80  43216  fourierdlem81  43217  rrndistlt  43320  sge0ltfirpmpt2  43453  sge0pnfmpt  43472  hoidmv1le  43621  hoidmvle  43627  vonioolem2  43708  smflimlem3  43794  euabsneu  44008  funressnfv  44023  aiotaval  44040  reuf1odnf  44053  reuf1od  44054  afvpcfv0  44092  dfafn5a  44106  afvelrnb  44109  afvelrnb0  44110  dfaimafn2  44112  dfatsnafv2  44198  dfatdmfcoafv2  44200  f1oresf1o2  44237  0nelsetpreimafv  44297  fargshiftfo  44349  sprsymrelf1  44403  reupr  44429  fmtnorec2lem  44449  fmtnoprmfac1  44472  fmtnoprmfac2  44474  sfprmdvdsmersenne  44510  lighneallem2  44513  dfeven2  44556  dfodd3  44557  odd2np1ALTV  44581  even3prm2  44626  fppr2odd  44638  nnsum3primesgbe  44699  nnsum3primesle9  44701  isomuspgrlem2d  44738  0nodd  44819  2nodd  44821  lmod0rng  44881  rngcinv  44994  rngcinvALTV  45006  ringcinv  45045  ringcinvALTV  45069  lcoel0  45224  lindslinindimp2lem4  45257  ldepspr  45269  lincresunit3  45277  nn0sumshdiglemB  45421  nn0sumshdiglem1  45422  rrx2pnedifcoorneorr  45518  eenglngeehlnmlem1  45538  eenglngeehlnmlem2  45539  rrx2linest  45543  rrx2linest2  45545  rrxsphere  45549  line2ylem  45552  line2x  45555  itscnhlc0xyqsol  45566  itschlc0xyqsol1  45567  itsclinecirc0b  45575  2itscp  45582  inlinecirc02plem  45587