Theorem eqcom 2763

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

Syntax hints:   ↔ wb 208   = wceq 1554

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1809  ax-4 1823  ax-5 1924  ax-6 1981  ax-7 2022  ax-9 2146  ax-ext 2728

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1794  df-cleq 2748

This theorem is referenced by:  eqcoms  2764  eqcomi  2765  neqcomd  2766  eqeq2d  2767  eqabcbw  2830  eqabcb  2896  necom  3004  nesym  3007  gencbvex  3504  clel5  3619  eqsbc2  3802  dfss  3918  sspsstri  4054  ssdifim  4220  disj4  4407  reuprg0  4655  preq1b  4798  invdisj  5080  disjprg  5090  dtruALT  5339  reusv3  5356  opthg2  5441  copsex2g  5456  copsex4g  5458  opcom  5464  opeqsng  5466  opeqpr  5468  snopeqop  5469  propeqop  5470  opthwiener  5477  vopelopabsb  5493  opthprc  5704  elxp3  5706  relop  5815  dmopab3  5888  rnopab3  5925  rncoeq  5951  restidsing  6032  somin1  6110  xpcan  6151  xpcan2  6152  dfrel4v  6165  dmsnn0  6183  reu3op  6268  reuop  6269  opreu2reurex  6270  ordtri2  6370  ordtri2or3  6437  suc11  6444  on0eqel  6460  snsn0non  6461  iota1  6489  iotan0  6500  sniota  6501  mptfnf  6645  fresaunres1  6726  dffn5  6914  fvelrnb  6916  dfimafn2  6919  funimass4  6920  feqmptdf  6926  fnsnfv  6935  dmfco  6952  funcnvmpt  6966  fndmdif  7012  fneqeql  7016  rexrn  7057  ralrn  7058  elrnrexdmb  7060  dffo4  7073  fssrescdmd  7097  funopsn  7119  funopsnOLD  7120  ftpg  7128  fprb  7167  ralima  7210  reximaOLD  7212  ralimaOLD  7213  fvclss  7214  dff13  7227  f1eqcocnv  7274  fnssintima  7335  imaeqsexvOLD  7336  riotaeqimp  7368  eusvobj2  7377  f1ocnvfv3  7380  oprabidw  7416  oprabid  7417  oprabv  7445  eloprabga  7494  ovelimab  7563  onmindif2  7779  br1steqg  7981  br2ndeqg  7982  dfoprab3  8024  opiota  8029  f1o2ndf1  8089  soseq  8127  brtpos2  8200  tpossym  8226  mpocurryd  8237  rdglim2  8391  tz7.48lem  8400  oaf1o  8520  omopthi  8619  erth2  8722  brecop  8780  erovlem  8783  ecopovsym  8789  eceqoveq  8792  xpcomco  9028  omxpenlem  9039  mapen  9102  nneneq  9163  unxpdomlem3  9191  unfilem1  9238  mapfien  9344  supgtoreq  9407  wemapsolem  9488  suc11reg  9564  inf3lem2  9574  inf3lem6  9578  ttrcltr  9661  djulf1o  9860  djurf1o  9861  infenaleph  10037  isinfcard  10038  dfac5  10075  cfeq0  10203  cfsuc  10204  ssfin4  10257  fin23lem25  10271  fin23lem22  10274  fin23lem40  10298  fin1a2lem5  10351  axcclem  10404  brdom7disj  10478  brdom6disj  10479  inar1  10723  psslinpr  10979  ltexprlem4  10987  ltsrpr  11025  mulgt0sr  11053  elreal  11079  ltresr  11088  leloe  11259  eqlei2  11284  addsubeq4  11435  subcan2  11446  negcon1  11473  negcon2  11474  addid0  11596  addeq0  11600  divmul2  11839  conjmul  11898  rereccl  11899  creur  12179  creui  12180  ind1a  12196  nndiv  12249  nn0sub  12521  elnn0z  12571  elznn0  12573  xrleloe  13136  ngtmnft  13159  icoshftf1o  13468  iccf1o  13490  fzen  13536  fzneuz  13603  injresinj  13787  fleqceilz  13854  mod0  13876  modmuladdnn0  13918  modirr  13945  addmodlteq  13949  nn0ennn  13982  hashrabsn01  14376  hashsdom  14384  hashgt12el2  14426  hashbclem  14455  hashfacen  14457  hashf1lem1  14458  hashtpg  14488  tpf1o  14504  fi1uzind  14510  ccatw2s1p1  14640  wrd2ind  14726  cshw1  14825  cshwsexa  14827  scshwfzeqfzo  14829  s2f1o  14919  wwlktovfo  14961  dmtrclfv  15021  cjreb  15126  leabs  15302  reusq0  15468  incexc2  15844  rpnnen2lem12  16233  dvdsval2  16265  dvdsabseq  16323  dvdsflip  16327  odd2np1  16351  oddm1even  16353  sqoddm1div8z  16364  m1exp1  16386  divalglem4  16406  divalglem8  16410  divalgb  16414  modremain  16418  zeqzmulgcd  16520  dfgcd2  16556  lcmfpr  16637  lcmftp  16646  lcmfunsnlem2  16650  divgcdcoprm0  16675  prm2orodd  16701  hashdvds  16786  oddprmdvds  16915  vdwlem12  17004  cshwshashlem1  17107  cshwsiun  17111  initoid  18010  termoid  18011  setcinv  18099  yonedainv  18289  joinfval  18379  joinfval2  18380  meetfval  18393  meetfval2  18394  latnle  18481  chnfi  18642  sgrp2nmndlem3  18938  grpid  18993  grpinvcnv  19024  grplmulf1o  19031  grpraddf1o  19032  grpsubeq0  19044  grpsubadd  19046  grplactcnv  19061  ressmulgnnd  19096  isnsg4  19184  eqg0el  19200  cycsubmel  19217  conjghm  19265  conjnmzb  19269  gacan  19321  gapm  19322  cntzrec  19352  oppgcntz  19380  fvcosymgeq  19445  odmulgeq  19573  dfod2  19580  sylow3lem3  19645  sylow3lem6  19648  lssnle  19690  lsmhash  19721  efgredlemb  19762  efgrelexlemb  19766  dprd2d2  20062  ablfac1eulem  20090  pgpfac1lem2  20093  pgpfac1lem4  20096  dvdsrval  20382  dvdsr02  20393  01eq0ring  20552  0ring01eqbi  20554  rngcinv  20659  ringcinv  20693  orngsqr  20888  rmodislmodlem  20969  lvecinv  21156  rngqiprngimf1lem  21337  rspsn  21376  prmirredlem  21497  zndvds  21574  znleval  21579  psrbagconf1o  21954  mplmonmul  22062  gsummoncoe1  22344  evl1maprhm  22415  mat1dimelbas  22504  mat1dimbas  22505  1mavmul  22581  ma1repveval  22604  mulmarep1gsum1  22606  mdetunilem9  22653  m2cpminvid2lem  22787  pmatcollpw3lem  22816  mp2pm2mplem4  22842  toponsspwpw  22955  dmtopon  22956  cmpfi  23441  ssref  23545  qtopeu  23749  hmeoimaf1o  23803  txhmeo  23836  fbasrn  23917  rnelfmlem  23985  hauspwpwf1  24020  alexsubALTlem4  24083  qustgpopn  24153  qustgphaus  24156  fmucndlem  24323  isngp3  24631  isngp4  24645  metnrmlem1a  24892  icopnfcnv  24977  iccpnfcnv  24979  ivthle  25491  ivthle2  25492  dyadmbl  25635  mbfinf  25700  i1fmulclem  25737  itg1mulc  25739  mvth  26027  dvivth  26045  lhop2  26050  r1pid2  26195  dvdsq1p  26196  reeff1o  26480  coseq1  26560  recosf1o  26570  resinf1o  26571  efopn  26693  cxpeq  26792  logreclem  26797  affineequiv  26858  affineequiv4  26861  affineequivne  26862  quad2  26874  dcubic  26881  mcubic  26882  quart  26896  atandm2  26912  rlimcnp2  27001  amgm  27025  wilthlem2  27103  mumullem2  27214  sqff1o  27216  dvdsflf1o  27221  gausslemma2dlem0i  27398  lgseisenlem2  27410  lgsquadlem2  27415  2lgslem1c  27427  2lgsoddprmlem2  27443  2lgsoddprm  27450  2sq2  27467  addsq2reu  27474  2sqreultlem  27481  2sqreunnltlem  27484  2sqreulem3  27487  ltsval2  27690  ltsintdifex  27695  ltsres  27696  nosepon  27699  noextenddif  27702  nosepssdm  27720  nogt01o  27730  nosupprefixmo  27734  noinfprefixmo  27735  nosupno  27737  noinfno  27752  lesloe  27788  eqcuts2  27849  cutbdaylt  27861  elold  27922  made0  27926  lrrecfr  28006  subadds  28133  oncutlt  28327  z12sge0  28546  renegscl  28561  tgjustf  28612  legtrid  28730  legso  28738  islmib  28926  lmicom  28927  lmiinv  28931  lmimid  28933  lmiopp  28941  colinearalglem2  29047  colinearalg  29050  ax5seglem4  29072  ax5seglem5  29073  axlowdimlem13  29094  axeuclidlem  29102  axeuclid  29103  axcontlem2  29105  axcontlem4  29107  elntg2  29125  structiedg0val  29162  uspgredgiedg  29315  uspgriedgedg  29316  usgredgsscusgredg  29599  fusgrn0degnn0  29639  umgr2v2evtxel  29662  vdiscusgrb  29670  uspgr2wlkeq  29785  wlk0prc  29792  wlklenvclwlk  29793  wlkp1lem8  29818  spthdep  29873  usgr2pthlem  29902  usgr2pth  29903  wlkiswwlksupgr2  30016  wlklnwwlkln2lem  30021  wwlksnextproplem3  30050  umgr2adedgwlk  30084  umgr2adedgspth  30087  umgr2wlkon  30089  usgrwwlks2on  30097  umgrwwlks2on  30098  elwwlks2  30108  elwspths2spth  30109  clwlkclwwlklem2a4  30138  clwlkclwwlklem2  30141  erclwwlkref  30161  clwwlkf  30188  erclwwlknref  30210  erclwwlknsym  30211  erclwwlkntr  30212  hashecclwwlkn1  30218  umgrhashecclwwlk  30219  eupth2lem2  30360  eucrct2eupth  30386  numclwwlkqhash  30516  isgrpo  30639  hvsubaddi  31208  hire  31236  shmodsi  31531  omlsilem  31544  chcon1i  31607  chnlei  31627  pjoml3i  31728  cmbr2i  31738  chscllem2  31780  adjsym  31975  eigorthi  31979  dfadj2  32027  adjval2  32033  cnvadj  32034  dmadjrnb  32048  adjvalval  32079  cnlnadjeui  32219  cnlnssadj  32222  adjbdln  32225  pjimai  32318  pjin2i  32335  pjin3i  32336  stadd3i  32390  largei  32409  cvnbtwn3  32430  cvnbtwn4  32431  mddmd2  32451  superpos  32496  atnemeq0  32519  sumdmdii  32557  sumdmdlem  32560  addltmulALT  32588  opreu2reuALT  32617  foresf1o  32645  difeq  32659  disjrdx  32733  fcoinvbr  32747  brab2d  32750  fmptco1f1o  32778  dfimafnf  32781  curry2ima  32854  intimafv  32856  receqid  32889  elicoelioo  32923  fzo0opth  32948  wrdt2ind  33085  swrdrn3  33087  gsummptp1  33191  gsummulsubdishift1  33202  cntrval2  33305  domnprodeq0  33414  qusker  33489  dvdsrspss  33527  lsmsnorb  33531  1arithufdlem4  33697  r1pid2OLD  33759  selvply1rhmlemb  33770  psrmonmul  33801  esplyind  33826  algextdeglem8  33975  zarcls  34125  xrmulc1cn  34181  xrge0iifcnv  34184  esumfsup  34321  esumpcvgval  34329  esumcvg  34337  esum2dlem  34343  issgon  34374  eulerpartgbij  34623  eulerpartlemgh  34629  ballotlemsima  34767  bnj1366  35081  bnj553  35150  bnj964  35195  fineqvnttrclse  35375  cusgredgex  35420  revwlk  35423  loop1cycl  35435  subfacp1lem3  35480  subfacp1lem5  35482  erdszelem9  35497  prv1n  35729  ply1divalg3  35940  quad3  35968  br6  36055  elintfv  36063  dfon2lem5  36083  dfon2lem8  36086  brbigcup  36194  dfbigcup2  36195  elfix  36199  ellimits  36206  snelsingles  36218  dfiota3  36219  imageval  36226  brapply  36234  lemsuccf  36237  dfsuccf2  36239  funpartlem  36240  brfullfun  36246  dfrecs2  36248  dfrdg4  36249  altopthbg  36266  altopthc  36269  altopthd  36270  altopelaltxp  36274  brsegle  36406  outsideofrflx  36425  elicc3  36625  nn0prpw  36631  opnregcld  36638  cldregopn  36639  fneval  36660  topfneec  36663  knoppndvlem9  36906  bj-elgab  37372  bj-gabima  37373  bj-elsngl  37401  bj-snglc  37402  bj-projval  37429  bj-disj2r  37461  bj-restreg  37537  bj-0int  37539  copsex2gd  37578  copsex2b  37580  bj-inftyexpitaudisj  37645  bj-inftyexpidisj  37650  bj-bary1lem1  37751  topdifinffinlem  37789  topdifinfeq  37792  fvineqsnf1  37852  curf  38045  uncf  38046  curunc  38049  unccur  38050  poimirlem2  38069  poimirlem16  38083  poimirlem17  38084  poimirlem19  38086  poimirlem20  38087  poimirlem27  38094  mblfinlem2  38105  mbfresfi  38113  itg2addnclem2  38119  ftc1anclem3  38142  fdc  38192  heibor1  38257  opidonOLD  38299  0rngo  38474  smprngopr  38499  isfldidl  38515  isfldidl2  38516  eqbrb  38686  eqelb  38688  ideq2  38760  relcnveq  38775  n0elqs  38779  disjressuc2  38858  dfsucmap3  38910  dfsucmap4  38912  dmsucmap  38915  preuniqval  38943  elrelscnveq  39075  qseq  39180  disjdmqscossss  39353  lcvnbtwn3  39600  lcvexchlem1  39606  lsatnem0  39617  opcon1b  39770  omllaw2N  39816  cmtbr2N  39825  leatb  39864  cvlsupr2  39915  glbconxN  39950  islln3  40082  llnexatN  40093  islpln3  40105  lplnexatN  40135  islvol3  40148  dalem-cly  40243  isline4N  40349  2llnma3r  40360  poml4N  40525  4atex2  40649  4atex2-0bOLDN  40651  cdlemefrs29bpre0  40968  cdlemftr3  41137  cdlemb3  41178  cdlemg17h  41240  cdlemg17pq  41244  cdlemg19  41256  cdlemg21  41258  tendoex  41547  dva1dim  41557  dihglb2  41914  doch11  41945  dochsordN  41946  lcfrlem9  42122  hlhillcs  42530  lcmineqlem4  42597  aks6d1c7lem2  42746  aks5lem3a  42754  aks5lem6  42757  unitscyglem2  42761  unitscyglem3  42762  addsubeq4com  42837  ef11d  42896  redivmul2d  43003  fimgmcyclem  43099  fsuppind  43120  elrfirn  43224  isnacs2  43235  isnacs3  43239  fiphp3d  43344  wopprc  43555  islnm2  43603  kercvrlsm  43608  fgraphopab  43728  tfsconcatlem  43861  tfsconcatrn  43867  tfsconcat0i  43870  tfsconcat0b  43871  tfsconcatrev  43873  oaun3lem1  43899  oadif1lem  43904  oadif1  43905  rp-fakeuninass  44040  snen1g  44048  iscard4  44057  sqrtcval  44165  frege124d  44285  frege129d  44287  frege92  44479  dffrege99  44486  clsk3nimkb  44564  clsk1indlem4  44568  clsk1indlem1  44569  ntrclsiso  44591  ntrclsk3  44594  ntrclsk13  44595  ntrneik4w  44624  extoimad  44688  int-sqdefd  44705  int-sqgeq0d  44710  radcnvrat  44838  bcc0  44864  opelopab4  45075  eqsbc2VD  45363  fzisoeu  45827  iuneqfzuz  45859  supxrleubrnmptf  45973  rexanuz2nf  46014  fsummulc1f  46095  fsumiunss  46099  fmul01lt1lem2  46109  sumnnodd  46154  fnlimfvre2  46199  limsupreuz  46259  limsupvaluz2  46260  liminfvalxr  46305  icccncfext  46409  cncfiooicc  46416  cncfioobdlem  46418  dvmptmulf  46459  dvmptfprodlem  46466  volioc  46494  itgioocnicc  46499  fourierdlem12  46641  fourierdlem20  46649  fourierdlem25  46654  fourierdlem33  46662  fourierdlem42  46671  fourierdlem52  46680  fourierdlem54  46682  fourierdlem57  46685  fourierdlem58  46686  fourierdlem59  46687  fourierdlem63  46691  fourierdlem65  46693  fourierdlem68  46696  fourierdlem73  46701  fourierdlem74  46702  fourierdlem75  46703  fourierdlem80  46708  fourierdlem81  46709  rrndistlt  46812  sge0ltfirpmpt2  46948  sge0pnfmpt  46967  hoidmv1le  47116  hoidmvle  47122  vonioolem2  47203  smflimlem3  47295  chnsubseqwl  47403  cos5teq  47422  lambert0  47429  lamberte  47430  euabsneu  47570  funressnfv  47585  aiotaval  47637  reuf1odnf  47649  reuf1od  47650  afvpcfv0  47688  dfafn5a  47702  afvelrnb  47705  afvelrnb0  47706  dfaimafn2  47708  dfatsnafv2  47794  dfatdmfcoafv2  47796  f1oresf1o2  47833  ceilbi  47879  minusmodnep2tmod  47901  0nelsetpreimafv  47944  fargshiftfo  47996  sprsymrelf1  48050  reupr  48076  nprmmul1  48081  fmtnorec2lem  48099  fmtnoprmfac1  48122  fmtnoprmfac2  48124  sfprmdvdsmersenne  48160  lighneallem2  48163  dfeven2  48219  dfodd3  48220  odd2np1ALTV  48244  even3prm2  48289  fppr2odd  48301  nnsum3primesgbe  48362  nnsum3primesle9  48364  clnbgrsym  48408  dfvopnbgr2  48423  isuspgrim0  48464  isuspgrimlem  48465  dfgric2  48485  grtriprop  48511  uspgrlimlem3  48560  gpgvtxedg1  48634  pgnbgreunbgrlem2lem1  48684  pgnbgreunbgrlem2lem2  48685  0nodd  48740  2nodd  48742  lmod0rng  48799  rngcinvALTV  48846  ringcinvALTV  48880  lcoel0  48998  lindslinindimp2lem4  49031  ldepspr  49043  lincresunit3  49051  nn0sumshdiglemB  49190  nn0sumshdiglem1  49191  rrx2pnedifcoorneorr  49287  eenglngeehlnmlem1  49307  eenglngeehlnmlem2  49308  rrx2linest  49312  rrx2linest2  49314  rrxsphere  49318  line2ylem  49321  line2x  49324  itscnhlc0xyqsol  49335  itschlc0xyqsol1  49336  itsclinecirc0b  49344  2itscp  49351  inlinecirc02plem  49356  brab2dd  49397  uptr2  49790