Theorem eqcom 2770

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

Syntax hints:   ↔ wb 209   = wceq 1570

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755

This theorem is referenced by:  eqcoms  2771  eqcomi  2772  neqcomd  2773  eqeq2d  2774  eqabcbw  2837  eqabcb  2903  necom  3011  nesym  3014  gencbvex  3511  clel5  3624  eqsbc2  3807  dfss  3924  sspsstri  4060  ssdifim  4226  disj4  4419  reuprg0  4668  preq1b  4811  invdisj  5095  disjprg  5105  dtruALT  5359  reusv3  5376  opthg2  5461  copsex2g  5476  copsex4g  5478  opcom  5484  opeqsng  5486  opeqpr  5488  snopeqop  5489  propeqop  5490  opthwiener  5497  vopelopabsb  5513  brab2d  5522  opthprc  5725  elxp3  5727  relop  5836  dmopab3  5909  rnopab3  5946  rncoeq  5971  restidsing  6055  somin1  6133  xpcan  6174  xpcan2  6175  dfrel4v  6188  dmsnn0  6208  reu3op  6293  reuop  6294  opreu2reurex  6295  ordtri2  6396  ordtri2or3  6463  suc11  6470  on0eqel  6486  snsn0non  6487  iota1  6515  iotan0  6526  sniota  6527  mptfnf  6670  fresaunres1  6751  dffn5  6939  fvelrnb  6941  dfimafn2  6944  funimass4  6945  feqmptdf  6951  fnsnfv  6960  dmfco  6977  funcnvmpt  6991  fndmdif  7037  fneqeql  7041  rexrn  7082  ralrn  7083  elrnrexdmb  7085  dffo4  7098  fssrescdmd  7122  funopsn  7144  funopsnOLD  7145  ftpg  7153  fprb  7192  ralima  7235  reximaOLD  7237  ralimaOLD  7238  fvclss  7239  dff13  7252  f1eqcocnv  7299  fnssintima  7360  imaeqsexvOLD  7361  riotaeqimp  7393  eusvobj2  7402  f1ocnvfv3  7405  oprabidw  7441  oprabid  7442  oprabv  7470  eloprabga  7519  ovelimab  7588  onmindif2  7802  br1steqg  8004  br2ndeqg  8005  dfoprab3  8047  opiota  8052  f1o2ndf1  8113  soseq  8151  brtpos2  8224  tpossym  8250  mpocurryd  8261  rdglim2  8415  tz7.48lem  8424  oaf1o  8544  omopthi  8643  erth2  8746  brecop  8804  erovlem  8807  ecopovsym  8813  eceqoveq  8816  xpcomco  9051  omxpenlem  9062  mapen  9125  nneneq  9186  unxpdomlem3  9214  unfilem1  9261  mapfien  9364  supgtoreq  9427  wemapsolem  9508  suc11reg  9584  inf3lem2  9594  inf3lem6  9598  ttrcltr  9681  djulf1o  9894  djurf1o  9895  infenaleph  10071  isinfcard  10072  dfac5  10108  cfeq0  10235  cfsuc  10236  ssfin4  10289  fin23lem25  10303  fin23lem22  10306  fin23lem40  10330  fin1a2lem5  10383  axcclem  10436  brdom7disj  10510  brdom6disj  10511  inar1  10755  psslinpr  11011  ltexprlem4  11019  ltsrpr  11057  mulgt0sr  11085  elreal  11111  ltresr  11120  leloe  11291  eqlei2  11316  addsubeq4  11467  subcan2  11478  negcon1  11505  negcon2  11506  addid0  11628  addeq0  11632  divmul2  11871  conjmul  11927  rereccl  11928  creur  12207  creui  12208  ind1a  12224  nndiv  12277  nn0sub  12549  elnn0z  12599  elznn0  12601  xrleloe  13164  ngtmnft  13187  icoshftf1o  13496  iccf1o  13518  fzen  13564  fzneuz  13632  injresinj  13816  fleqceilz  13883  mod0  13905  modmuladdnn0  13947  modirr  13974  addmodlteq  13978  nn0ennn  14011  hashrabsn01  14405  hashsdom  14413  hashgt12el2  14456  hashbclem  14485  hashfacen  14487  hashf1lem1  14488  hashtpg  14518  tpf1o  14534  fi1uzind  14540  ccatw2s1p1  14670  wrd2ind  14756  cshw1  14855  cshwsexa  14857  scshwfzeqfzo  14859  s2f1o  14949  wwlktovfo  14991  dmtrclfv  15051  cjreb  15170  leabs  15346  reusq0  15512  incexc2  15888  rpnnen2lem12  16276  dvdsval2  16308  dvdsabseq  16366  dvdsflip  16370  odd2np1  16394  oddm1even  16396  sqoddm1div8z  16407  m1exp1  16429  divalglem4  16449  divalglem8  16453  divalgb  16457  modremain  16461  zeqzmulgcd  16563  dfgcd2  16599  lcmfpr  16680  lcmftp  16689  lcmfunsnlem2  16693  divgcdcoprm0  16718  prm2orodd  16744  hashdvds  16829  oddprmdvds  16958  vdwlem12  17047  cshwshashlem1  17150  cshwsiun  17154  initoid  18053  termoid  18054  setcinv  18142  yonedainv  18332  joinfval  18422  joinfval2  18423  meetfval  18436  meetfval2  18437  latnle  18524  chnfi  18685  sgrp2nmndlem3  18982  grpid  19037  grpinvcnv  19068  grplmulf1o  19074  grpraddf1o  19075  grpsubeq0  19087  grpsubadd  19089  grplactcnv  19104  ressmulgnnd  19139  isnsg4  19228  eqg0el  19249  cycsubmel  19266  conjghm  19314  conjnmzb  19318  gacan  19370  gapm  19371  cntzrec  19401  oppgcntz  19429  fvcosymgeq  19494  odmulgeq  19622  dfod2  19629  sylow3lem3  19694  sylow3lem6  19697  lssnle  19739  lsmhash  19770  efgredlemb  19811  efgrelexlemb  19815  dprd2d2  20111  ablfac1eulem  20139  pgpfac1lem2  20142  pgpfac1lem4  20145  dvdsrval  20439  dvdsr02  20450  01eq0ring  20628  0ring01eqbi2  20630  0ring01eqbi  20631  rngcinv  20736  ringcinv  20770  orngsqr  20969  rmodislmodlem  21050  lvecinv  21237  isfieldidl2  21387  rngqiprngimf1lem  21434  rspsn  21501  prmirredlem  21622  zndvds  21699  znleval  21704  psrbagconf1o  22079  mplmonmul  22187  gsummoncoe1  22468  evl1maprhm  22539  mat1dimelbas  22628  mat1dimbas  22629  1mavmul  22705  ma1repveval  22728  mulmarep1gsum1  22730  mdetunilem9  22777  m2cpminvid2lem  22911  pmatcollpw3lem  22940  mp2pm2mplem4  22966  toponsspwpw  23079  dmtopon  23080  cmpfi  23565  ssref  23669  qtopeu  23873  hmeoimaf1o  23927  txhmeo  23960  fbasrn  24041  rnelfmlem  24109  hauspwpwf1  24144  alexsubALTlem4  24207  qustgpopn  24277  qustgphaus  24280  fmucndlem  24447  isngp3  24755  isngp4  24769  metnrmlem1a  25016  icopnfcnv  25101  iccpnfcnv  25103  ivthle  25615  ivthle2  25616  dyadmbl  25759  mbfinf  25824  i1fmulclem  25861  itg1mulc  25863  mvth  26151  dvivth  26169  lhop2  26174  r1pid2  26319  dvdsq1p  26320  reeff1o  26610  coseq1  26690  recosf1o  26700  resinf1o  26701  efopn  26823  cxpeq  26922  logreclem  26927  affineequiv  26988  affineequiv4  26991  affineequivne  26992  quad2  27004  dcubic  27011  mcubic  27012  quart  27026  atandm2  27042  rlimcnp2  27131  amgm  27155  wilthlem2  27233  mumullem2  27344  sqff1o  27346  dvdsflf1o  27351  gausslemma2dlem0i  27528  lgseisenlem2  27540  lgsquadlem2  27545  2lgslem1c  27557  2lgsoddprmlem2  27573  2lgsoddprm  27580  2sq2  27597  addsq2reu  27604  2sqreultlem  27611  2sqreunnltlem  27614  2sqreulem3  27617  ltsval2  27820  ltsintdifex  27825  ltsres  27826  nosepon  27829  noextenddif  27832  nosepssdm  27850  nogt01o  27860  nosupprefixmo  27864  noinfprefixmo  27865  nosupno  27867  noinfno  27882  lesloe  27918  eqcuts2  27979  cutbdaylt  27991  elold  28052  made0  28056  lrrecfr  28136  subadds  28263  oncutlt  28457  z12sge0  28676  renegscl  28691  tgjustf  28742  legtrid  28860  legso  28868  islmib  29096  lmicom  29097  lmiinv  29101  lmimid  29103  lmiopp  29112  prlngsym  29191  colinearalglem2  29257  colinearalg  29260  ax5seglem4  29282  ax5seglem5  29283  axlowdimlem13  29304  axeuclidlem  29312  axeuclid  29313  axcontlem2  29315  axcontlem4  29317  elntg2  29335  structiedg0val  29372  uspgredgiedg  29525  uspgriedgedg  29526  usgredgsscusgredg  29809  fusgrn0degnn0  29849  umgr2v2evtxel  29872  vdiscusgrb  29880  uspgr2wlkeq  29995  wlk0prc  30002  wlklenvclwlk  30003  wlkp1lem8  30028  spthdep  30083  usgr2pthlem  30112  usgr2pth  30113  wlkiswwlksupgr2  30226  wlklnwwlkln2lem  30231  wwlksnextproplem3  30260  umgr2adedgwlk  30294  umgr2adedgspth  30297  umgr2wlkon  30299  usgrwwlks2on  30307  umgrwwlks2on  30308  elwwlks2  30318  elwspths2spth  30319  clwlkclwwlklem2a4  30348  clwlkclwwlklem2  30351  erclwwlkref  30371  clwwlkf  30398  erclwwlknref  30420  erclwwlknsym  30421  erclwwlkntr  30422  hashecclwwlkn1  30428  umgrhashecclwwlk  30429  eupth2lem2  30570  eucrct2eupth  30596  numclwwlkqhash  30726  isgrpo  30849  hvsubaddi  31418  hire  31446  shmodsi  31741  omlsilem  31754  chcon1i  31817  chnlei  31837  pjoml3i  31938  cmbr2i  31948  chscllem2  31990  adjsym  32185  eigorthi  32189  dfadj2  32237  adjval2  32243  cnvadj  32244  dmadjrnb  32258  adjvalval  32289  cnlnadjeui  32429  cnlnssadj  32432  adjbdln  32435  pjimai  32528  pjin2i  32545  pjin3i  32546  stadd3i  32600  largei  32619  cvnbtwn3  32640  cvnbtwn4  32641  mddmd2  32661  superpos  32706  atnemeq0  32729  sumdmdii  32767  sumdmdlem  32770  addltmulALT  32798  opreu2reuALT  32823  foresf1o  32850  difeq  32864  disjrdx  32936  fcoinvbr  32950  fmptco1f1o  32978  dfimafnf  32981  curry2ima  33054  intimafv  33056  receqid  33089  elicoelioo  33123  fzo0opth  33148  wrdt2ind  33273  swrdrn3  33275  gsummptp1  33377  gsummulsubdishift1  33388  cntrval2  33491  domnprodeq0  33599  qusker  33669  dvdsrspss  33700  lsmsnorb  33704  1arithufdlem4  33837  selvply1rhmlemb  33909  psrmonmul  33940  esplyind  33965  algextdeglem8  34114  zarcls  34264  xrmulc1cn  34320  xrge0iifcnv  34323  esumfsup  34460  esumpcvgval  34468  esumcvg  34476  esum2dlem  34482  issgon  34513  eulerpartgbij  34762  eulerpartlemgh  34768  ballotlemsima  34906  bnj1366  35217  bnj553  35286  bnj964  35331  dfscott3  35512  fineqvnttrclse  35537  cusgredgex  35614  revwlk  35617  loop1cycl  35629  subfacp1lem3  35674  subfacp1lem5  35676  erdszelem9  35691  prv1n  35923  ply1divalg3  36134  quad3  36162  br6  36249  elintfv  36257  dfon2lem5  36277  dfon2lem8  36280  brbigcup  36388  dfbigcup2  36389  elfix  36393  ellimits  36400  snelsingles  36412  dfiota3  36413  imageval  36420  brapply  36428  lemsuccf  36431  dfsuccf2  36433  funpartlem  36434  brfullfun  36440  dfrecs2  36442  dfrdg4  36443  altopthbg  36460  altopthc  36463  altopthd  36464  altopelaltxp  36468  brsegle  36600  outsideofrflx  36619  elicc3  36848  nn0prpw  36854  opnregcld  36861  cldregopn  36862  fneval  36883  topfneec  36886  knoppndvlem9  37129  bj-elgab  37595  bj-gabima  37596  bj-elsngl  37624  bj-snglc  37625  bj-projval  37652  bj-disj2r  37684  bj-restreg  37761  bj-0int  37763  copsex2gd  37802  copsex2b  37804  bj-inftyexpitaudisj  37869  bj-inftyexpidisj  37874  bj-bary1lem1  37975  topdifinffinlem  38013  topdifinfeq  38016  fvineqsnf1  38076  curf  38269  uncf  38270  curunc  38273  unccur  38274  poimirlem2  38293  poimirlem16  38307  poimirlem17  38308  poimirlem19  38310  poimirlem20  38311  poimirlem27  38318  mblfinlem2  38329  mbfresfi  38337  itg2addnclem2  38343  ftc1anclem3  38366  fdc  38416  heibor1  38481  opidonOLD  38523  0rngo  38698  smprngopr  38723  isfldidl  38739  isfldidl2  38740  eqbrb  38908  eqelb  38910  ideq2  38982  relcnveq  38997  n0elqs  39001  disjressuc2  39080  dfsucmap3  39132  dfsucmap4  39134  dmsucmap  39137  preuniqval  39165  elrelscnveq  39297  qseq  39402  disjdmqscossss  39575  lcvnbtwn3  39822  lcvexchlem1  39828  lsatnem0  39839  opcon1b  39992  omllaw2N  40038  cmtbr2N  40047  leatb  40086  cvlsupr2  40137  glbconxN  40172  islln3  40304  llnexatN  40315  islpln3  40327  lplnexatN  40357  islvol3  40370  dalem-cly  40465  isline4N  40571  2llnma3r  40582  poml4N  40747  4atex2  40871  4atex2-0bOLDN  40873  cdlemefrs29bpre0  41190  cdlemftr3  41359  cdlemb3  41400  cdlemg17h  41462  cdlemg17pq  41466  cdlemg19  41478  cdlemg21  41480  tendoex  41769  dva1dim  41779  dihglb2  42136  doch11  42167  dochsordN  42168  lcfrlem9  42344  hlhillcs  42752  lcmineqlem4  42819  aks6d1c7lem2  42968  aks5lem3a  42976  aks5lem6  42979  unitscyglem2  42983  unitscyglem3  42984  addsubeq4com  43061  ef11d  43120  redivmul2d  43227  fimgmcyclem  43321  fsuppind  43342  elrfirn  43446  isnacs2  43457  isnacs3  43461  fiphp3d  43566  wopprc  43777  islnm2  43825  kercvrlsm  43830  fgraphopab  43950  tfsconcatlem  44083  tfsconcatrn  44089  tfsconcat0i  44092  tfsconcat0b  44093  tfsconcatrev  44095  oaun3lem1  44121  oadif1lem  44126  oadif1  44127  rp-fakeuninass  44262  snen1g  44270  iscard4  44279  sqrtcval  44387  frege124d  44507  frege129d  44509  frege92  44701  dffrege99  44708  clsk3nimkb  44786  clsk1indlem4  44790  clsk1indlem1  44791  ntrclsiso  44813  ntrclsk3  44816  ntrclsk13  44817  ntrneik4w  44846  extoimad  44910  int-sqdefd  44927  int-sqgeq0d  44932  radcnvrat  45044  bcc0  45070  opelopab4  45280  eqsbc2VD  45568  fzisoeu  46039  iuneqfzuz  46071  supxrleubrnmptf  46185  rexanuz2nf  46226  fsummulc1f  46307  fsumiunss  46311  fmul01lt1lem2  46321  sumnnodd  46366  fnlimfvre2  46411  limsupreuz  46471  limsupvaluz2  46472  liminfvalxr  46517  icccncfext  46621  cncfiooicc  46628  cncfioobdlem  46630  dvmptmulf  46671  dvmptfprodlem  46678  volioc  46706  itgioocnicc  46711  fourierdlem12  46853  fourierdlem20  46861  fourierdlem25  46866  fourierdlem33  46874  fourierdlem42  46883  fourierdlem52  46892  fourierdlem54  46894  fourierdlem57  46897  fourierdlem58  46898  fourierdlem59  46899  fourierdlem63  46903  fourierdlem65  46905  fourierdlem68  46908  fourierdlem73  46913  fourierdlem74  46914  fourierdlem75  46915  fourierdlem80  46920  fourierdlem81  46921  rrndistlt  47024  sge0ltfirpmpt2  47160  sge0pnfmpt  47179  hoidmv1le  47328  hoidmvle  47334  vonioolem2  47415  smflimlem3  47507  chnsubseqwl  47615  cos5teq  47637  lambert0  47644  lamberte  47645  euabsneu  47785  funressnfv  47800  aiotaval  47852  reuf1odnf  47864  reuf1od  47865  afvpcfv0  47903  dfafn5a  47917  afvelrnb  47920  afvelrnb0  47921  dfaimafn2  47923  dfatsnafv2  48009  dfatdmfcoafv2  48011  f1oresf1o2  48048  ceilbi  48094  minusmodnep2tmod  48116  0nelsetpreimafv  48159  fargshiftfo  48211  sprsymrelf1  48265  reupr  48291  nprmmul1  48296  fmtnorec2lem  48314  fmtnoprmfac1  48337  fmtnoprmfac2  48339  sfprmdvdsmersenne  48375  lighneallem2  48378  dfeven2  48434  dfodd3  48435  odd2np1ALTV  48459  even3prm2  48504  fppr2odd  48516  nnsum3primesgbe  48577  nnsum3primesle9  48579  clnbgrsym  48623  dfvopnbgr2  48638  isuspgrim0  48679  isuspgrimlem  48680  dfgric2  48700  grtriprop  48726  uspgrlimlem3  48775  gpgvtxedg1  48849  pgnbgreunbgrlem2lem1  48899  pgnbgreunbgrlem2lem2  48900  0nodd  48955  2nodd  48957  lmod0rng  49014  rngcinvALTV  49061  ringcinvALTV  49095  isidom3  49130  lcoel0  49228  lindslinindimp2lem4  49261  ldepspr  49273  lincresunit3  49281  nn0sumshdiglemB  49420  nn0sumshdiglem1  49421  rrx2pnedifcoorneorr  49517  eenglngeehlnmlem1  49537  eenglngeehlnmlem2  49538  rrx2linest  49542  rrx2linest2  49544  rrxsphere  49548  line2ylem  49551  line2x  49554  itscnhlc0xyqsol  49565  itschlc0xyqsol1  49566  itsclinecirc0b  49574  2itscp  49581  inlinecirc02plem  49586  brab2dd  49626  uptr2  50019