Theorem eqcom 2629

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

Syntax hints:   ↔ wb 196   = wceq 1483

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-cleq 2615

This theorem is referenced by:  eqcoms  2630  eqcomi  2631  eqeq2d  2632  eqtr2  2642  eqtr3  2643  abeq1  2733  necom  2847  nesym  2850  pm13.181  2876  gencbvex  3250  eqsbc3r  3492  eqsbc3rOLD  3493  dfss  3589  sspsstri  3709  ssnelpss  3718  dfss5OLD  3819  ssdifim  3862  disj4  4025  preq1b  4377  preqr1OLD  4380  invdisj  4638  disjprg  4648  reusv3  4876  dtruALT  4899  dtruALT2  4911  opthg2  4948  copsex4g  4959  opcom  4965  opeqsn  4967  opeqpr  4968  snopeqop  4969  propeqop  4970  opthwiener  4976  opthprc  5167  elxp3  5169  relop  5272  dmopab3  5337  rncoeq  5389  restidsing  5458  somin1  5529  xpcan  5570  xpcan2  5571  dfrel4v  5584  dmsnn0  5600  ordtri2  5758  ordtri2or3  5824  suc11  5831  on0eqel  5845  snsn0non  5846  iota1  5865  sniota  5878  mptfnf  6015  fresaunres1  6077  dffn5  6241  fvelrnb  6243  dfimafn2  6246  funimass4  6247  feqmptdf  6251  fnsnfv  6258  dmfco  6272  fndmdif  6321  fneqeql  6325  rexrn  6361  ralrn  6362  elrnrexdmb  6364  dffo4  6375  funopsn  6413  ftpg  6423  rexima  6497  ralima  6498  fvclss  6500  dff13  6512  f1eqcocnv  6556  riotaeqimp  6634  eusvobj2  6643  f1ocnvfv3  6646  oprabid  6677  oprabv  6703  eloprabga  6747  ovelimab  6812  onmindif2  7012  dfoprab3  7224  opiota  7229  f1o2ndf1  7285  brtpos2  7358  tpossym  7384  mpt2curryd  7395  rdglim2  7528  tz7.48lem  7536  oaf1o  7643  omopthi  7737  erth2  7792  brecop  7840  erovlem  7843  ecopovsym  7849  eceqoveq  7853  xpcomco  8050  omxpenlem  8061  mapen  8124  nneneq  8143  unxpdomlem3  8166  unfilem1  8224  mapfien  8313  supgtoreq  8376  wemapsolem  8455  suc11reg  8516  inf3lem2  8526  inf3lem6  8530  infenaleph  8914  isinfcard  8915  dfac5  8951  cfeq0  9078  cfsuc  9079  ssfin4  9132  fin23lem25  9146  fin23lem22  9149  fin23lem40  9173  fin1a2lem5  9226  axcclem  9279  brdom7disj  9353  brdom6disj  9354  inar1  9597  psslinpr  9853  ltexprlem4  9861  ltsrpr  9898  mulgt0sr  9926  elreal  9952  ltresr  9961  leloe  10124  eqlei2  10148  addsubeq4  10296  subcan2  10306  negcon1  10333  negcon2  10334  addid0  10450  divmul2  10689  conjmul  10742  rereccl  10743  creur  11014  creui  11015  nndiv  11061  nn0sub  11343  elnn0z  11390  elznn0  11392  zq  11794  xrleloe  11977  ngtmnft  11997  icoshftf1o  12295  iccf1o  12316  fzen  12358  fzneuz  12421  4fvwrd4  12459  injresinj  12589  fleqceilz  12653  mod0  12675  modmuladdnn0  12714  modirr  12741  addmodlteq  12745  nn0ennn  12778  hashrabsn01  13162  hashsdom  13170  hashgt12el2  13211  hashbclem  13236  hashfacen  13238  hashf1lem1  13239  hashtpg  13267  fi1uzind  13279  fi1uzindOLD  13285  wrdlen1  13343  ccatw2s1p1  13413  wrd2ind  13477  cshwlen  13545  cshw1  13568  scshwfzeqfzo  13572  s2f1o  13661  wwlktovfo  13701  dmtrclfv  13759  cjreb  13863  leabs  14039  incexc2  14570  pwm1geoser  14600  rpnnen2lem12  14954  dvdsval2  14986  dvdsabseq  15035  dvdsflip  15039  odd2np1  15065  oddm1even  15067  sqoddm1div8z  15078  m1exp1  15093  divalglem4  15119  divalglem8  15123  divalgb  15127  divalgmodOLD  15130  modremain  15132  zeqzmulgcd  15232  dfgcd2  15263  lcmfpr  15340  lcmftp  15349  lcmfunsnlem2  15353  divgcdcoprm0  15379  prm2orodd  15404  hashdvds  15480  phisum  15495  oddprmdvds  15607  vdwlem12  15696  cshwshashlem1  15802  cshwsiun  15806  initoid  16655  termoid  16656  setcinv  16740  yonedainv  16921  joinfval  17001  joinfval2  17002  meetfval  17015  meetfval2  17016  latnle  17085  sgrp2nmndlem3  17412  grpid  17457  grpinvcnv  17483  grplmulf1o  17489  grpsubeq0  17501  grpsubadd  17503  grplactcnv  17518  isnsg4  17637  conjghm  17691  conjnmzb  17695  gacan  17738  gapm  17739  cntzrec  17766  oppgcntz  17794  symgmov1  17812  fvcosymgeq  17849  odmulgeq  17974  dfod2  17981  sylow3lem3  18044  sylow3lem6  18047  lssnle  18087  lsmhash  18118  efgredlemb  18159  efgrelexlemb  18163  gsumzoppg  18344  dprd2d2  18443  ablfac1eulem  18471  pgpfac1lem2  18474  pgpfac1lem4  18477  dvdsrval  18645  dvdsr02  18656  rmodislmodlem  18930  lvecinv  19113  rspsn  19254  0ring01eqbi  19273  psrbagconf1o  19374  mplmonmul  19464  gsummoncoe1  19674  prmirredlem  19841  zndvds  19898  znleval  19903  mat1dimelbas  20277  mat1dimbas  20278  1mavmul  20354  ma1repveval  20377  mulmarep1gsum1  20379  mdetunilem9  20426  m2cpminvid2lem  20559  pmatcollpw3lem  20588  mp2pm2mplem4  20614  toponsspwpw  20726  dmtopon  20727  cmpfi  21211  ssref  21315  qtopeu  21519  hmeoimaf1o  21573  txhmeo  21606  fbasrn  21688  rnelfmlem  21756  hauspwpwf1  21791  alexsubALTlem4  21854  qustgpopn  21923  qustgphaus  21926  fmucndlem  22095  isngp3  22402  isngp4  22416  metnrmlem1a  22661  icopnfcnv  22741  iccpnfcnv  22743  ivthle  23225  ivthle2  23226  dyadmbl  23368  mbfinf  23432  i1fmulclem  23469  itg1mulc  23471  mvth  23755  dvivth  23773  lhop2  23778  dvdsq1p  23920  reeff1o  24201  coseq1  24274  recosf1o  24281  resinf1o  24282  efopn  24404  cxpeq  24498  logreclem  24500  affineequiv  24553  quad2  24566  dcubic  24573  mcubic  24574  quart  24588  atandm2  24604  rlimcnp2  24693  amgm  24717  wilthlem2  24795  mumullem2  24906  sqff1o  24908  dvdsflf1o  24913  gausslemma2dlem0i  25089  lgseisenlem2  25101  lgsquadlem2  25106  2lgslem1c  25118  2lgsoddprmlem2  25134  2lgsoddprm  25141  legtrid  25486  legso  25494  islmib  25679  lmicom  25680  lmiinv  25684  lmimid  25686  lmiopp  25694  colinearalglem2  25787  colinearalg  25790  ax5seglem4  25812  ax5seglem5  25813  axlowdimlem13  25834  axeuclidlem  25842  axeuclid  25843  axcontlem2  25845  axcontlem4  25847  structiedg0val  25911  usgredgsscusgredg  26355  fusgrn0degnn0  26395  umgr2v2evtxel  26418  vdiscusgrb  26426  uspgr2wlkeq  26542  wlk0prc  26550  wlklenvclwlk  26551  wlkp1lem8  26577  spthdep  26630  usgr2pthlem  26659  usgr2pth  26660  wlkiswwlksupgr2  26763  wlklnwwlkln2lem  26768  wwlksnextproplem3  26806  umgr2adedgwlk  26841  umgr2adedgspth  26844  umgr2wlkon  26846  umgrwwlks2on  26850  elwwlks2  26861  elwspths2spth  26862  clwlkclwwlklem2a4  26898  clwlkclwwlklem2  26901  clwwlksf  26915  erclwwlksref  26934  erclwwlksnref  26946  erclwwlksnsym  26947  erclwwlksntr  26948  hashecclwwlksn1  26954  umgrhashecclwwlk  26955  clwlksfoclwwlk  26963  eupth2lem2  27079  eucrct2eupth  27105  isgrpo  27351  hvsubaddi  27923  hire  27951  shmodsi  28248  omlsilem  28261  chcon1i  28324  chnlei  28344  pjoml3i  28445  cmbr2i  28455  chscllem2  28497  adjsym  28692  eigorthi  28696  dfadj2  28744  adjval2  28750  cnvadj  28751  dmadjrnb  28765  adjvalval  28796  cnlnadjeui  28936  cnlnssadj  28939  adjbdln  28942  pjimai  29035  pjin2i  29052  pjin3i  29053  stadd3i  29107  largei  29126  cvnbtwn3  29147  cvnbtwn4  29148  mddmd2  29168  superpos  29213  atnemeq0  29236  sumdmdii  29274  sumdmdlem  29277  addltmulALT  29305  foresf1o  29343  difeq  29355  disjrdx  29404  fcoinvbr  29419  fmptco1f1o  29434  dfimafnf  29436  funcnvmptOLD  29467  funcnvmpt  29468  curry2ima  29486  cnvoprab  29498  addeq0  29510  elicoelioo  29540  orngsqr  29804  xrmulc1cn  29976  xrge0iifcnv  29979  ind1a  30081  esumfsup  30132  esumpcvgval  30140  esumcvg  30148  esum2dlem  30154  issgon  30186  eulerpartgbij  30434  eulerpartlemgh  30440  ballotlemsima  30577  bnj1366  30900  bnj553  30968  bnj964  31013  subfacp1lem3  31164  subfacp1lem5  31166  erdszelem9  31181  quad3  31564  br6  31647  elintfv  31662  fprb  31669  br1steq  31670  br2ndeq  31671  br1steqg  31672  br2ndeqg  31673  dfon2lem5  31692  dfon2lem8  31695  soseq  31751  sltval2  31809  sltintdifex  31814  sltres  31815  nosepon  31818  noextenddif  31821  nosepssdm  31836  nosupno  31849  sleloe  31879  scutbdaylt  31922  brbigcup  32005  dfbigcup2  32006  elfix  32010  ellimits  32017  snelsingles  32029  dfiota3  32030  imageval  32037  brapply  32045  brsuccf  32048  funpartlem  32049  brfullfun  32055  dfrecs2  32057  dfrdg4  32058  altopthbg  32075  altopthc  32078  altopthd  32079  altopelaltxp  32083  brsegle  32215  outsideofrflx  32234  elicc3  32311  nn0prpw  32318  opnregcld  32325  cldregopn  32326  fneval  32347  topfneec  32350  knoppndvlem9  32511  bj-abeq1  32774  bj-elsngl  32956  bj-snglc  32957  bj-projval  32984  bj-disj2r  33013  bj-restreg  33052  bj-0int  33055  bj-inftyexpidisj  33097  bj-bary1lem1  33161  topdifinffinlem  33195  topdifinfeq  33198  curf  33387  uncf  33388  curunc  33391  unccur  33392  poimirlem2  33411  poimirlem16  33425  poimirlem17  33426  poimirlem19  33428  poimirlem20  33429  poimirlem27  33436  mblfinlem2  33447  mbfresfi  33456  itg2addnclem2  33462  ftc1anclem3  33487  fdc  33541  heibor1  33609  opidonOLD  33651  0rngo  33826  smprngopr  33851  isfldidl  33867  isfldidl2  33868  eqelb  34002  ideq2  34078  relcnveq  34093  n0elqs  34098  lcvnbtwn3  34315  lcvexchlem1  34321  lsatnem0  34332  opcon1b  34485  omllaw2N  34531  cmtbr2N  34540  leatb  34579  cvlsupr2  34630  glbconxN  34664  islln3  34796  llnexatN  34807  islpln3  34819  lplnexatN  34849  islvol3  34862  dalem-cly  34957  isline4N  35063  2llnma3r  35074  poml4N  35239  4atex2  35363  4atex2-0bOLDN  35365  cdlemefrs29bpre0  35684  cdlemftr3  35853  cdlemb3  35894  cdlemg17h  35956  cdlemg17pq  35960  cdlemg19  35972  cdlemg21  35974  tendoex  36263  dva1dim  36273  dihglb2  36631  doch11  36662  dochsordN  36663  lcfrlem9  36839  hlhillcs  37250  elrfirn  37258  isnacs2  37269  isnacs3  37273  fiphp3d  37383  wopprc  37597  islnm2  37648  kercvrlsm  37653  fgraphopab  37788  rp-fakeuninass  37862  frege124d  38053  frege129d  38055  frege92  38249  dffrege99  38256  clsk3nimkb  38338  clsk1indlem4  38342  clsk1indlem1  38343  ntrclsiso  38365  ntrclsk3  38368  ntrclsk13  38369  ntrneik4w  38398  extoimad  38464  int-sqdefd  38484  int-sqgeq0d  38489  radcnvrat  38513  bcc0  38539  opelopab4  38767  eqsbc3rVD  39075  fzisoeu  39514  iuneqfzuz  39551  supxrleubrnmptf  39680  fsummulc1f  39802  fsumiunss  39807  fmul01lt1lem2  39817  sumnnodd  39862  fnlimfvre2  39909  limsupreuz  39969  limsupvaluz2  39970  liminfvalxr  40015  icccncfext  40100  cncfiooicc  40107  cncfioobdlem  40109  dvmptmulf  40152  dvmptfprodlem  40159  volioc  40188  itgioocnicc  40193  fourierdlem12  40336  fourierdlem20  40344  fourierdlem25  40349  fourierdlem33  40357  fourierdlem42  40366  fourierdlem52  40375  fourierdlem54  40377  fourierdlem57  40380  fourierdlem58  40381  fourierdlem59  40382  fourierdlem63  40386  fourierdlem65  40388  fourierdlem68  40391  fourierdlem73  40396  fourierdlem74  40397  fourierdlem75  40398  fourierdlem80  40403  fourierdlem81  40404  rrndistlt  40510  sge0ltfirpmpt2  40643  sge0pnfmpt  40662  hoidmv1le  40808  hoidmvle  40814  vonioolem2  40895  smflimlem3  40981  funressnfv  41208  afvpcfv0  41226  dfafn5a  41240  afvelrnb  41243  afvelrnb0  41244  dfaimafn2  41246  fargshiftfo  41378  fmtnorec2lem  41454  fmtnoprmfac1  41477  fmtnoprmfac2  41479  sfprmdvdsmersenne  41520  lighneallem2  41523  dfeven2  41562  dfodd3  41563  odd2np1ALTV  41585  even3prm2  41628  nnsum3primesgbe  41680  nnsum3primesle9  41682  sprsymrelf1  41746  0nodd  41810  2nodd  41812  lmod0rng  41868  rngcinv  41981  rngcinvALTV  41993  ringcinv  42032  ringcinvALTV  42056  lcoel0  42217  lindslinindimp2lem4  42250  ldepspr  42262  lincresunit3  42270  nn0sumshdiglemB  42414  nn0sumshdiglem1  42415