Theorem eqcom 2776

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

Syntax hints:   ↔ wb 209   = wceq 1567

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-cleq 2761

This theorem is referenced by:  eqcoms  2777  eqcomi  2778  neqcomd  2779  eqeq2d  2780  eqabcbw  2843  eqabcb  2909  necom  3017  nesym  3020  gencbvex  3519  clel5  3633  eqsbc2  3816  dfss  3932  sspsstri  4068  ssdifim  4234  disj4  4425  reuprg0  4673  preq1b  4815  invdisj  5099  disjprg  5109  dtruALT  5360  reusv3  5377  opthg2  5462  copsex2g  5477  copsex4g  5479  opcom  5485  opeqsng  5487  opeqpr  5489  snopeqop  5490  propeqop  5491  opthwiener  5498  vopelopabsb  5514  brab2d  5523  opthprc  5726  elxp3  5728  relop  5837  dmopab3  5910  rnopab3  5947  rncoeq  5972  restidsing  6056  somin1  6134  xpcan  6175  xpcan2  6176  dfrel4v  6189  dmsnn0  6209  reu3op  6294  reuop  6295  opreu2reurex  6296  ordtri2  6397  ordtri2or3  6464  suc11  6471  on0eqel  6487  snsn0non  6488  iota1  6516  iotan0  6527  sniota  6528  mptfnf  6671  fresaunres1  6752  dffn5  6940  fvelrnb  6942  dfimafn2  6945  funimass4  6946  feqmptdf  6952  fnsnfv  6961  dmfco  6978  funcnvmpt  6992  fndmdif  7038  fneqeql  7042  rexrn  7083  ralrn  7084  elrnrexdmb  7086  dffo4  7099  fssrescdmd  7123  funopsn  7145  funopsnOLD  7146  ftpg  7154  fprb  7193  ralima  7236  reximaOLD  7238  ralimaOLD  7239  fvclss  7240  dff13  7253  f1eqcocnv  7300  fnssintima  7361  imaeqsexvOLD  7362  riotaeqimp  7394  eusvobj2  7403  f1ocnvfv3  7406  oprabidw  7442  oprabid  7443  oprabv  7471  eloprabga  7520  ovelimab  7589  onmindif2  7805  br1steqg  8007  br2ndeqg  8008  dfoprab3  8050  opiota  8055  f1o2ndf1  8116  soseq  8154  brtpos2  8227  tpossym  8253  mpocurryd  8264  rdglim2  8418  tz7.48lem  8427  oaf1o  8547  omopthi  8646  erth2  8749  brecop  8807  erovlem  8810  ecopovsym  8816  eceqoveq  8819  xpcomco  9054  omxpenlem  9065  mapen  9128  nneneq  9189  unxpdomlem3  9217  unfilem1  9264  mapfien  9367  supgtoreq  9430  wemapsolem  9511  suc11reg  9587  inf3lem2  9597  inf3lem6  9601  ttrcltr  9684  djulf1o  9897  djurf1o  9898  infenaleph  10074  isinfcard  10075  dfac5  10111  cfeq0  10239  cfsuc  10240  ssfin4  10293  fin23lem25  10307  fin23lem22  10310  fin23lem40  10334  fin1a2lem5  10387  axcclem  10440  brdom7disj  10514  brdom6disj  10515  inar1  10759  psslinpr  11015  ltexprlem4  11023  ltsrpr  11061  mulgt0sr  11089  elreal  11115  ltresr  11124  leloe  11295  eqlei2  11320  addsubeq4  11471  subcan2  11482  negcon1  11509  negcon2  11510  addid0  11632  addeq0  11636  divmul2  11875  conjmul  11931  rereccl  11932  creur  12211  creui  12212  ind1a  12228  nndiv  12281  nn0sub  12553  elnn0z  12603  elznn0  12605  xrleloe  13168  ngtmnft  13191  icoshftf1o  13500  iccf1o  13522  fzen  13568  fzneuz  13635  injresinj  13819  fleqceilz  13886  mod0  13908  modmuladdnn0  13950  modirr  13977  addmodlteq  13981  nn0ennn  14014  hashrabsn01  14408  hashsdom  14416  hashgt12el2  14459  hashbclem  14488  hashfacen  14490  hashf1lem1  14491  hashtpg  14521  tpf1o  14537  fi1uzind  14543  ccatw2s1p1  14673  wrd2ind  14759  cshw1  14858  cshwsexa  14860  scshwfzeqfzo  14862  s2f1o  14952  wwlktovfo  14994  dmtrclfv  15054  cjreb  15173  leabs  15349  reusq0  15515  incexc2  15891  rpnnen2lem12  16280  dvdsval2  16312  dvdsabseq  16370  dvdsflip  16374  odd2np1  16398  oddm1even  16400  sqoddm1div8z  16411  m1exp1  16433  divalglem4  16453  divalglem8  16457  divalgb  16461  modremain  16465  zeqzmulgcd  16567  dfgcd2  16603  lcmfpr  16684  lcmftp  16693  lcmfunsnlem2  16697  divgcdcoprm0  16722  prm2orodd  16748  hashdvds  16833  oddprmdvds  16962  vdwlem12  17051  cshwshashlem1  17154  cshwsiun  17158  initoid  18057  termoid  18058  setcinv  18146  yonedainv  18336  joinfval  18426  joinfval2  18427  meetfval  18440  meetfval2  18441  latnle  18528  chnfi  18689  sgrp2nmndlem3  18986  grpid  19041  grpinvcnv  19072  grplmulf1o  19078  grpraddf1o  19079  grpsubeq0  19091  grpsubadd  19093  grplactcnv  19108  ressmulgnnd  19143  isnsg4  19232  eqg0el  19253  cycsubmel  19270  conjghm  19318  conjnmzb  19322  gacan  19374  gapm  19375  cntzrec  19405  oppgcntz  19433  fvcosymgeq  19498  odmulgeq  19626  dfod2  19633  sylow3lem3  19698  sylow3lem6  19701  lssnle  19743  lsmhash  19774  efgredlemb  19815  efgrelexlemb  19819  dprd2d2  20115  ablfac1eulem  20143  pgpfac1lem2  20146  pgpfac1lem4  20149  dvdsrval  20442  dvdsr02  20453  01eq0ring  20613  0ring01eqbi2  20615  0ring01eqbi  20616  rngcinv  20721  ringcinv  20755  orngsqr  20946  rmodislmodlem  21027  lvecinv  21214  rngqiprngimf1lem  21404  rspsn  21469  prmirredlem  21590  zndvds  21667  znleval  21672  psrbagconf1o  22047  mplmonmul  22155  gsummoncoe1  22436  evl1maprhm  22507  mat1dimelbas  22596  mat1dimbas  22597  1mavmul  22673  ma1repveval  22696  mulmarep1gsum1  22698  mdetunilem9  22745  m2cpminvid2lem  22879  pmatcollpw3lem  22908  mp2pm2mplem4  22934  toponsspwpw  23047  dmtopon  23048  cmpfi  23533  ssref  23637  qtopeu  23841  hmeoimaf1o  23895  txhmeo  23928  fbasrn  24009  rnelfmlem  24077  hauspwpwf1  24112  alexsubALTlem4  24175  qustgpopn  24245  qustgphaus  24248  fmucndlem  24415  isngp3  24723  isngp4  24737  metnrmlem1a  24984  icopnfcnv  25069  iccpnfcnv  25071  ivthle  25583  ivthle2  25584  dyadmbl  25727  mbfinf  25792  i1fmulclem  25829  itg1mulc  25831  mvth  26119  dvivth  26137  lhop2  26142  r1pid2  26287  dvdsq1p  26288  reeff1o  26575  coseq1  26655  recosf1o  26665  resinf1o  26666  efopn  26788  cxpeq  26887  logreclem  26892  affineequiv  26953  affineequiv4  26956  affineequivne  26957  quad2  26969  dcubic  26976  mcubic  26977  quart  26991  atandm2  27007  rlimcnp2  27096  amgm  27120  wilthlem2  27198  mumullem2  27309  sqff1o  27311  dvdsflf1o  27316  gausslemma2dlem0i  27493  lgseisenlem2  27505  lgsquadlem2  27510  2lgslem1c  27522  2lgsoddprmlem2  27538  2lgsoddprm  27545  2sq2  27562  addsq2reu  27569  2sqreultlem  27576  2sqreunnltlem  27579  2sqreulem3  27582  ltsval2  27785  ltsintdifex  27790  ltsres  27791  nosepon  27794  noextenddif  27797  nosepssdm  27815  nogt01o  27825  nosupprefixmo  27829  noinfprefixmo  27830  nosupno  27832  noinfno  27847  lesloe  27883  eqcuts2  27944  cutbdaylt  27956  elold  28017  made0  28021  lrrecfr  28101  subadds  28228  oncutlt  28422  z12sge0  28641  renegscl  28656  tgjustf  28707  legtrid  28825  legso  28833  islmib  29053  lmicom  29054  lmiinv  29058  lmimid  29060  lmiopp  29068  prlngsym  29145  colinearalglem2  29197  colinearalg  29200  ax5seglem4  29222  ax5seglem5  29223  axlowdimlem13  29244  axeuclidlem  29252  axeuclid  29253  axcontlem2  29255  axcontlem4  29257  elntg2  29275  structiedg0val  29312  uspgredgiedg  29465  uspgriedgedg  29466  usgredgsscusgredg  29749  fusgrn0degnn0  29789  umgr2v2evtxel  29812  vdiscusgrb  29820  uspgr2wlkeq  29935  wlk0prc  29942  wlklenvclwlk  29943  wlkp1lem8  29968  spthdep  30023  usgr2pthlem  30052  usgr2pth  30053  wlkiswwlksupgr2  30166  wlklnwwlkln2lem  30171  wwlksnextproplem3  30200  umgr2adedgwlk  30234  umgr2adedgspth  30237  umgr2wlkon  30239  usgrwwlks2on  30247  umgrwwlks2on  30248  elwwlks2  30258  elwspths2spth  30259  clwlkclwwlklem2a4  30288  clwlkclwwlklem2  30291  erclwwlkref  30311  clwwlkf  30338  erclwwlknref  30360  erclwwlknsym  30361  erclwwlkntr  30362  hashecclwwlkn1  30368  umgrhashecclwwlk  30369  eupth2lem2  30510  eucrct2eupth  30536  numclwwlkqhash  30666  isgrpo  30789  hvsubaddi  31358  hire  31386  shmodsi  31681  omlsilem  31694  chcon1i  31757  chnlei  31777  pjoml3i  31878  cmbr2i  31888  chscllem2  31930  adjsym  32125  eigorthi  32129  dfadj2  32177  adjval2  32183  cnvadj  32184  dmadjrnb  32198  adjvalval  32229  cnlnadjeui  32369  cnlnssadj  32372  adjbdln  32375  pjimai  32468  pjin2i  32485  pjin3i  32486  stadd3i  32540  largei  32559  cvnbtwn3  32580  cvnbtwn4  32581  mddmd2  32601  superpos  32646  atnemeq0  32669  sumdmdii  32707  sumdmdlem  32710  addltmulALT  32738  opreu2reuALT  32763  foresf1o  32790  difeq  32804  disjrdx  32876  fcoinvbr  32890  fmptco1f1o  32918  dfimafnf  32921  curry2ima  32994  intimafv  32996  receqid  33029  elicoelioo  33063  fzo0opth  33088  wrdt2ind  33213  swrdrn3  33215  gsummptp1  33317  gsummulsubdishift1  33328  cntrval2  33431  domnprodeq0  33539  qusker  33611  dvdsrspss  33643  lsmsnorb  33647  1arithufdlem4  33781  selvply1rhmlemb  33853  psrmonmul  33884  esplyind  33909  algextdeglem8  34058  zarcls  34208  xrmulc1cn  34264  xrge0iifcnv  34267  esumfsup  34404  esumpcvgval  34412  esumcvg  34420  esum2dlem  34426  issgon  34457  eulerpartgbij  34706  eulerpartlemgh  34712  ballotlemsima  34850  bnj1366  35161  bnj553  35230  bnj964  35275  fineqvnttrclse  35459  cusgredgex  35512  revwlk  35515  loop1cycl  35527  subfacp1lem3  35572  subfacp1lem5  35574  erdszelem9  35589  prv1n  35821  ply1divalg3  36032  quad3  36060  br6  36147  elintfv  36155  dfon2lem5  36175  dfon2lem8  36178  brbigcup  36286  dfbigcup2  36287  elfix  36291  ellimits  36298  snelsingles  36310  dfiota3  36311  imageval  36318  brapply  36326  lemsuccf  36329  dfsuccf2  36331  funpartlem  36332  brfullfun  36338  dfrecs2  36340  dfrdg4  36341  altopthbg  36358  altopthc  36361  altopthd  36362  altopelaltxp  36366  brsegle  36498  outsideofrflx  36517  elicc3  36716  nn0prpw  36722  opnregcld  36729  cldregopn  36730  fneval  36751  topfneec  36754  knoppndvlem9  36997  bj-elgab  37462  bj-gabima  37463  bj-elsngl  37491  bj-snglc  37492  bj-projval  37519  bj-disj2r  37551  bj-restreg  37628  bj-0int  37630  copsex2gd  37669  copsex2b  37671  bj-inftyexpitaudisj  37736  bj-inftyexpidisj  37741  bj-bary1lem1  37842  topdifinffinlem  37880  topdifinfeq  37883  fvineqsnf1  37943  curf  38136  uncf  38137  curunc  38140  unccur  38141  poimirlem2  38160  poimirlem16  38174  poimirlem17  38175  poimirlem19  38177  poimirlem20  38178  poimirlem27  38185  mblfinlem2  38196  mbfresfi  38204  itg2addnclem2  38210  ftc1anclem3  38233  fdc  38283  heibor1  38348  opidonOLD  38390  0rngo  38565  smprngopr  38590  isfldidl  38606  isfldidl2  38607  eqbrb  38777  eqelb  38779  ideq2  38851  relcnveq  38866  n0elqs  38870  disjressuc2  38949  dfsucmap3  39001  dfsucmap4  39003  dmsucmap  39006  preuniqval  39034  elrelscnveq  39166  qseq  39271  disjdmqscossss  39444  lcvnbtwn3  39691  lcvexchlem1  39697  lsatnem0  39708  opcon1b  39861  omllaw2N  39907  cmtbr2N  39916  leatb  39955  cvlsupr2  40006  glbconxN  40041  islln3  40173  llnexatN  40184  islpln3  40196  lplnexatN  40226  islvol3  40239  dalem-cly  40334  isline4N  40440  2llnma3r  40451  poml4N  40616  4atex2  40740  4atex2-0bOLDN  40742  cdlemefrs29bpre0  41059  cdlemftr3  41228  cdlemb3  41269  cdlemg17h  41331  cdlemg17pq  41335  cdlemg19  41347  cdlemg21  41349  tendoex  41638  dva1dim  41648  dihglb2  42005  doch11  42036  dochsordN  42037  lcfrlem9  42213  hlhillcs  42621  lcmineqlem4  42688  aks6d1c7lem2  42837  aks5lem3a  42845  aks5lem6  42848  unitscyglem2  42852  unitscyglem3  42853  addsubeq4com  42930  ef11d  42989  redivmul2d  43096  fimgmcyclem  43192  fsuppind  43213  elrfirn  43317  isnacs2  43328  isnacs3  43332  fiphp3d  43437  wopprc  43648  islnm2  43696  kercvrlsm  43701  fgraphopab  43821  tfsconcatlem  43954  tfsconcatrn  43960  tfsconcat0i  43963  tfsconcat0b  43964  tfsconcatrev  43966  oaun3lem1  43992  oadif1lem  43997  oadif1  43998  rp-fakeuninass  44133  snen1g  44141  iscard4  44150  sqrtcval  44258  frege124d  44378  frege129d  44380  frege92  44572  dffrege99  44579  clsk3nimkb  44657  clsk1indlem4  44661  clsk1indlem1  44662  ntrclsiso  44684  ntrclsk3  44687  ntrclsk13  44688  ntrneik4w  44717  extoimad  44781  int-sqdefd  44798  int-sqgeq0d  44803  radcnvrat  44915  bcc0  44941  opelopab4  45151  eqsbc2VD  45439  fzisoeu  45910  iuneqfzuz  45942  supxrleubrnmptf  46056  rexanuz2nf  46097  fsummulc1f  46178  fsumiunss  46182  fmul01lt1lem2  46192  sumnnodd  46237  fnlimfvre2  46282  limsupreuz  46342  limsupvaluz2  46343  liminfvalxr  46388  icccncfext  46492  cncfiooicc  46499  cncfioobdlem  46501  dvmptmulf  46542  dvmptfprodlem  46549  volioc  46577  itgioocnicc  46582  fourierdlem12  46724  fourierdlem20  46732  fourierdlem25  46737  fourierdlem33  46745  fourierdlem42  46754  fourierdlem52  46763  fourierdlem54  46765  fourierdlem57  46768  fourierdlem58  46769  fourierdlem59  46770  fourierdlem63  46774  fourierdlem65  46776  fourierdlem68  46779  fourierdlem73  46784  fourierdlem74  46785  fourierdlem75  46786  fourierdlem80  46791  fourierdlem81  46792  rrndistlt  46895  sge0ltfirpmpt2  47031  sge0pnfmpt  47050  hoidmv1le  47199  hoidmvle  47205  vonioolem2  47286  smflimlem3  47378  chnsubseqwl  47486  cos5teq  47505  lambert0  47512  lamberte  47513  euabsneu  47653  funressnfv  47668  aiotaval  47720  reuf1odnf  47732  reuf1od  47733  afvpcfv0  47771  dfafn5a  47785  afvelrnb  47788  afvelrnb0  47789  dfaimafn2  47791  dfatsnafv2  47877  dfatdmfcoafv2  47879  f1oresf1o2  47916  ceilbi  47962  minusmodnep2tmod  47984  0nelsetpreimafv  48027  fargshiftfo  48079  sprsymrelf1  48133  reupr  48159  nprmmul1  48164  fmtnorec2lem  48182  fmtnoprmfac1  48205  fmtnoprmfac2  48207  sfprmdvdsmersenne  48243  lighneallem2  48246  dfeven2  48302  dfodd3  48303  odd2np1ALTV  48327  even3prm2  48372  fppr2odd  48384  nnsum3primesgbe  48445  nnsum3primesle9  48447  clnbgrsym  48491  dfvopnbgr2  48506  isuspgrim0  48547  isuspgrimlem  48548  dfgric2  48568  grtriprop  48594  uspgrlimlem3  48643  gpgvtxedg1  48717  pgnbgreunbgrlem2lem1  48767  pgnbgreunbgrlem2lem2  48768  0nodd  48823  2nodd  48825  lmod0rng  48882  rngcinvALTV  48929  ringcinvALTV  48963  lcoel0  49092  lindslinindimp2lem4  49125  ldepspr  49137  lincresunit3  49145  nn0sumshdiglemB  49284  nn0sumshdiglem1  49285  rrx2pnedifcoorneorr  49381  eenglngeehlnmlem1  49401  eenglngeehlnmlem2  49402  rrx2linest  49406  rrx2linest2  49408  rrxsphere  49412  line2ylem  49415  line2x  49418  itscnhlc0xyqsol  49429  itschlc0xyqsol1  49430  itsclinecirc0b  49438  2itscp  49445  inlinecirc02plem  49450  brab2dd  49490  uptr2  49883