Theorem eqcom 2617

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

Syntax hints:   ↔ wb 195   = wceq 1475

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-cleq 2603

This theorem is referenced by:  eqcoms  2618  eqcomi  2619  eqeq2d  2620  eqtr2  2630  eqtr3  2631  abeq1  2720  necom  2835  nesym  2838  pm13.181  2864  gencbvex  3223  eqsbc3r  3459  eqsbc3rOLD  3460  dfss  3555  sspsstri  3671  ssnelpss  3680  dfss5OLD  3781  disj4  3977  preq1b  4317  preqr1OLD  4320  invdisj  4571  disjprg  4578  reusv3  4802  dtruALT  4826  dtruALT2  4838  opthg2  4874  copsex4g  4885  opcom  4890  opeqsn  4892  opeqpr  4893  snopeqop  4894  propeqop  4895  opthwiener  4901  opthprc  5089  elxp3  5092  relop  5194  dmopab3  5259  rncoeq  5310  restidsing  5377  somin1  5448  xpcan  5489  xpcan2  5490  dfrel4v  5503  dmsnn0  5518  ordtri2  5675  ordtri2or3  5741  suc11  5748  on0eqel  5762  snsn0non  5763  iota1  5782  sniota  5795  mptfnf  5928  fresaunres1  5990  dffn5  6151  fvelrnb  6153  dfimafn2  6156  funimass4  6157  feqmptdf  6161  fnsnfv  6168  dmfco  6182  fndmdif  6229  fneqeql  6233  rexrn  6269  ralrn  6270  elrnrexdmb  6272  dffo4  6283  funopsn  6319  ftpg  6328  rexima  6401  ralima  6402  fvclss  6404  dff13  6416  f1eqcocnv  6456  eusvobj2  6542  f1ocnvfv3  6545  oprabid  6576  oprabv  6601  eloprabga  6645  ovelimab  6710  onmindif2  6904  dfoprab3  7115  opiota  7118  f1o2ndf1  7172  brtpos2  7245  tpossym  7271  mpt2curryd  7282  rdglim2  7415  tz7.48lem  7423  oaf1o  7530  omopthi  7624  erth2  7679  brecop  7727  erovlem  7730  ecopovsym  7736  eceqoveq  7740  xpcomco  7935  omxpenlem  7946  mapen  8009  nneneq  8028  unxpdomlem3  8051  unfilem1  8109  mapfien  8196  supgtoreq  8259  wemapsolem  8338  suc11reg  8399  inf3lem2  8409  inf3lem6  8413  infenaleph  8797  isinfcard  8798  dfac5  8834  cfeq0  8961  cfsuc  8962  ssfin4  9015  fin23lem25  9029  fin23lem22  9032  fin23lem40  9056  fin1a2lem5  9109  axcclem  9162  brdom7disj  9234  brdom6disj  9235  inar1  9476  psslinpr  9732  ltexprlem4  9740  ltsrpr  9777  mulgt0sr  9805  elreal  9831  ltresr  9840  leloe  10003  eqlei2  10027  addsubeq4  10175  subcan2  10185  negcon1  10212  negcon2  10213  addid0  10329  divmul2  10568  conjmul  10621  rereccl  10622  creur  10891  creui  10892  nndiv  10938  nn0sub  11220  elnn0z  11267  elznn0  11269  zq  11670  xrleloe  11853  ngtmnft  11872  icoshftf1o  12166  iccf1o  12187  fzen  12229  fzneuz  12290  4fvwrd4  12328  injresinj  12451  fleqceilz  12515  mod0  12537  modmuladdnn0  12576  modirr  12603  addmodlteq  12607  nn0ennn  12640  hashrabsn01  13023  hashsdom  13031  hashgt12el2  13071  hashbclem  13093  hashfacen  13095  hashf1lem1  13096  hashtpg  13121  fi1uzind  13134  fi1uzindOLD  13140  wrdlen1  13198  ccatw2s1p1  13265  wrd2ind  13329  cshwlen  13396  cshw1  13419  scshwfzeqfzo  13423  s2f1o  13511  wwlktovfo  13549  dmtrclfv  13607  cjreb  13711  leabs  13887  incexc2  14409  pwm1geoser  14439  rpnnen2lem12  14793  dvdsval2  14824  dvdsabseq  14873  dvdsflip  14877  odd2np1  14903  oddm1even  14905  sqoddm1div8z  14916  m1exp1  14931  divalglem4  14957  divalglem8  14961  divalgb  14965  divalgmodOLD  14968  modremain  14970  zeqzmulgcd  15070  dfgcd2  15101  lcmfpr  15178  lcmftp  15187  lcmfunsnlem2  15191  divgcdcoprm0  15217  prm2orodd  15242  hashdvds  15318  phisum  15333  oddprmdvds  15445  vdwlem12  15534  cshwshashlem1  15640  cshwsiun  15644  initoid  16478  termoid  16479  setcinv  16563  yonedainv  16744  joinfval  16824  joinfval2  16825  meetfval  16838  meetfval2  16839  latnle  16908  sgrp2nmndlem3  17235  grpid  17280  grpinvcnv  17306  grplmulf1o  17312  grpsubeq0  17324  grpsubadd  17326  grplactcnv  17341  isnsg4  17460  conjghm  17514  conjnmzb  17518  gacan  17561  gapm  17562  cntzrec  17589  oppgcntz  17617  symgmov1  17635  fvcosymgeq  17672  odmulgeq  17797  dfod2  17804  sylow3lem3  17867  sylow3lem6  17870  lssnle  17910  lsmhash  17941  efgredlemb  17982  efgrelexlemb  17986  gsumzoppg  18167  dprd2d2  18266  ablfac1eulem  18294  pgpfac1lem2  18297  pgpfac1lem4  18300  dvdsrval  18468  dvdsr02  18479  lvecinv  18934  rspsn  19075  0ring01eqbi  19094  psrbagconf1o  19195  mplmonmul  19285  gsummoncoe1  19495  prmirredlem  19660  zndvds  19717  znleval  19722  mat1dimelbas  20096  mat1dimbas  20097  1mavmul  20173  ma1repveval  20196  mulmarep1gsum1  20198  mdetunilem9  20245  m2cpminvid2lem  20378  pmatcollpw3lem  20407  mp2pm2mplem4  20433  cmpfi  21021  ssref  21125  qtopeu  21329  hmeoimaf1o  21383  txhmeo  21416  fbasrn  21498  rnelfmlem  21566  hauspwpwf1  21601  alexsubALTlem4  21664  qustgpopn  21733  qustgphaus  21736  fmucndlem  21905  isngp3  22212  isngp4  22226  metnrmlem1a  22469  icopnfcnv  22549  iccpnfcnv  22551  ivthle  23032  ivthle2  23033  dyadmbl  23174  mbfinf  23238  i1fmulclem  23275  itg1mulc  23277  mvth  23559  dvivth  23577  lhop2  23582  dvdsq1p  23724  reeff1o  24005  coseq1  24078  recosf1o  24085  resinf1o  24086  efopn  24204  cxpeq  24298  logreclem  24300  affineequiv  24353  quad2  24366  dcubic  24373  mcubic  24374  quart  24388  atandm2  24404  rlimcnp2  24493  amgm  24517  wilthlem2  24595  mumullem2  24706  sqff1o  24708  dvdsflf1o  24713  gausslemma2dlem0i  24889  lgseisenlem2  24901  lgsquadlem2  24906  2lgslem1c  24918  2lgsoddprmlem2  24934  2lgsoddprm  24941  legtrid  25286  legso  25294  islmib  25479  lmicom  25480  lmiinv  25484  lmimid  25486  lmiopp  25494  colinearalglem2  25587  colinearalg  25590  ax5seglem4  25612  ax5seglem5  25613  axlowdimlem13  25634  axeuclidlem  25642  axeuclid  25643  axcontlem2  25645  axcontlem4  25647  structiedg0val  25699  nbgraop1  25954  nbgraf1olem1  25970  nbgraf1olem5  25974  nbcusgra  25992  uvtxnb  26025  usgra2adedgwlkonALT  26144  fargshiftfo  26166  wlklniswwlkn2  26228  usg2wlkeq  26236  wwlkextproplem3  26271  clwlkisclwwlklem2a4  26312  clwlkisclwwlklem1  26315  clwwlkf  26322  clwwnisshclwwn  26337  erclwwlkref  26341  erclwwlknref  26353  erclwwlknsym  26354  erclwwlkntr  26355  hashecclwwlkn1  26361  usghashecclwwlk  26362  wlklenvclwlk  26366  clwlkfoclwwlk  26372  el2wlkonot  26396  el2spthonot  26397  el2wlkonotot0  26399  eupatrl  26495  eupath2lem2  26505  usgn0fidegnn0  26556  frgrawopreg2  26578  frg2woteqm  26586  frgregordn0  26597  isgrpo  26735  hvsubaddi  27307  hire  27335  shmodsi  27632  omlsilem  27645  chcon1i  27708  chnlei  27728  pjoml3i  27829  cmbr2i  27839  chscllem2  27881  adjsym  28076  eigorthi  28080  dfadj2  28128  adjval2  28134  cnvadj  28135  dmadjrnb  28149  adjvalval  28180  cnlnadjeui  28320  cnlnssadj  28323  adjbdln  28326  pjimai  28419  pjin2i  28436  pjin3i  28437  stadd3i  28491  largei  28510  cvnbtwn3  28531  cvnbtwn4  28532  mddmd2  28552  superpos  28597  atnemeq0  28620  sumdmdii  28658  sumdmdlem  28661  addltmulALT  28689  foresf1o  28727  difeq  28739  disjrdx  28786  disjunsn  28789  fcoinvbr  28799  dfimafnf  28817  funcnvmptOLD  28850  funcnvmpt  28851  curry2ima  28869  cnvoprab  28886  addeq0  28898  elicoelioo  28930  orngsqr  29135  xrmulc1cn  29304  xrge0iifcnv  29307  ind1a  29410  esumfsup  29459  esumpcvgval  29467  esumcvg  29475  esum2dlem  29481  issgon  29513  eulerpartgbij  29761  eulerpartlemgh  29767  ballotlemsima  29904  bnj1366  30154  bnj553  30222  bnj964  30267  subfacp1lem3  30418  subfacp1lem5  30420  erdszelem9  30435  quad3  30818  br6  30900  fprb  30916  br1steq  30917  br2ndeq  30918  dfon2lem5  30936  dfon2lem8  30939  soseq  30995  sltval2  31053  sltintdifex  31060  sltres  31061  nosepon  31066  nofulllem5  31105  brbigcup  31175  dfbigcup2  31176  elfix  31180  ellimits  31187  snelsingles  31199  dfiota3  31200  imageval  31207  brapply  31215  brsuccf  31218  funpartlem  31219  brfullfun  31225  dfrecs2  31227  dfrdg4  31228  altopthbg  31245  altopthc  31248  altopthd  31249  altopelaltxp  31253  brsegle  31385  outsideofrflx  31404  elicc3  31481  nn0prpw  31488  opnregcld  31495  cldregopn  31496  fneval  31517  topfneec  31520  knoppndvlem9  31681  bj-abeq1  31962  bj-elsngl  32149  bj-snglc  32150  bj-projval  32177  bj-restreg  32233  bj-toponss  32241  bj-dmtopon  32242  bj-inftyexpidisj  32274  bj-bary1lem1  32338  topdifinffinlem  32371  topdifinfeq  32374  curf  32557  uncf  32558  curunc  32561  unccur  32562  poimirlem2  32581  poimirlem16  32595  poimirlem17  32596  poimirlem19  32598  poimirlem20  32599  poimirlem27  32606  mblfinlem2  32617  mbfresfi  32626  itg2addnclem2  32632  ftc1anclem3  32657  fdc  32711  heibor1  32779  opidonOLD  32821  0rngo  32996  smprngopr  33021  isfldidl  33037  isfldidl2  33038  lcvnbtwn3  33333  lcvexchlem1  33339  lsatnem0  33350  opcon1b  33503  omllaw2N  33549  cmtbr2N  33558  leatb  33597  cvlsupr2  33648  glbconxN  33682  islln3  33814  llnexatN  33825  islpln3  33837  lplnexatN  33867  islvol3  33880  dalem-cly  33975  isline4N  34081  2llnma3r  34092  poml4N  34257  4atex2  34381  4atex2-0bOLDN  34383  cdlemefrs29bpre0  34702  cdlemftr3  34871  cdlemb3  34912  cdlemg17h  34974  cdlemg17pq  34978  cdlemg19  34990  cdlemg21  34992  tendoex  35281  dva1dim  35291  dihglb2  35649  doch11  35680  dochsordN  35681  lcfrlem9  35857  hlhillcs  36268  elrfirn  36276  isnacs2  36287  isnacs3  36291  fiphp3d  36401  wopprc  36615  islnm2  36666  kercvrlsm  36671  fgraphopab  36807  rp-fakeuninass  36881  frege124d  37072  frege129d  37074  frege92  37269  dffrege99  37276  clsk3nimkb  37358  clsk1indlem4  37362  clsk1indlem1  37363  ntrclsiso  37385  ntrclsk3  37388  ntrclsk13  37389  ntrneik4w  37418  extoimad  37486  int-rightdistd  37505  int-sqdefd  37506  int-sqgeq0d  37511  radcnvrat  37535  bcc0  37561  opelopab4  37788  eqsbc3rVD  38097  fzisoeu  38455  iuneqfzuz  38492  fsummulc1f  38635  fsumiunss  38642  fmul01lt1lem2  38652  sumnnodd  38697  fnlimfvre2  38744  icccncfext  38773  cncfiooicc  38780  cncfioobdlem  38782  dvmptmulf  38827  dvmptfprodlem  38834  volioc  38864  itgioocnicc  38869  fourierdlem12  39012  fourierdlem20  39020  fourierdlem25  39025  fourierdlem33  39033  fourierdlem42  39042  fourierdlem52  39051  fourierdlem54  39053  fourierdlem57  39056  fourierdlem58  39057  fourierdlem59  39058  fourierdlem63  39062  fourierdlem65  39064  fourierdlem68  39067  fourierdlem73  39072  fourierdlem74  39073  fourierdlem75  39074  fourierdlem80  39079  fourierdlem81  39080  rrndistlt  39186  sge0ltfirpmpt2  39319  sge0pnfmpt  39338  hoidmv1le  39484  hoidmvle  39490  vonioolem2  39572  smflimlem3  39659  funressnfv  39857  afvpcfv0  39875  dfafn5a  39889  afvelrnb  39892  afvelrnb0  39893  dfaimafn2  39895  fmtnorec2lem  39992  fmtnoprmfac1  40015  fmtnoprmfac2  40017  sfprmdvdsmersenne  40058  lighneallem2  40061  dfeven2  40100  dfodd3  40101  odd2np1ALTV  40123  nnsum3primesgbe  40208  nnsum3primesle9  40210  riotaeqimp  40338  usgredgsscusgredg  40675  fusgrn0degnn0  40714  umgr2v2evtxel  40738  vdiscusgrb  40746  uspgr2wlkeq  40854  1wlk0prc  40862  1wlklenvclwlk  40863  1wlkp1lem8  40889  spthdep  40940  usgr2pthlem  40969  usgr2pth  40970  1wlkiswwlksupgr2  41074  1wlklnwwlkln2lem  41079  wwlksnextproplem3  41117  umgr2adedgwlk  41152  umgr2adedgspth  41155  umgr2wlkon  41157  umgrwwlks2on  41161  elwwlks2  41170  elwspths2spth  41171  clwlkclwwlklem2a4  41206  clwlkclwwlklem2  41209  clwwlksf  41222  erclwwlksref  41241  erclwwlksnref  41253  erclwwlksnsym  41254  erclwwlksntr  41255  hashecclwwlksn1  41261  umgrhashecclwwlk  41262  clwlksfoclwwlk  41270  eupth2lem2  41387  eucrct2eupth  41413  frgrwopreg2  41488  frgr2wwlkeqm  41496  frrusgrord0  41503  av-extwwlkfablem2  41510  0nodd  41600  2nodd  41602  lmod0rng  41658  rngcinv  41773  rngcinvALTV  41785  ringcinv  41824  ringcinvALTV  41848  lcoel0  42011  lindslinindimp2lem4  42044  ldepspr  42056  lincresunit3  42064  nn0sumshdiglemB  42212  nn0sumshdiglem1  42213