Theorem eqcom 2742

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

Syntax hints:   ↔ wb 206   = wceq 1540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2727

This theorem is referenced by:  eqcoms  2743  eqcomi  2744  neqcomd  2745  eqeq2d  2746  eqabcb  2876  necom  2985  nesym  2988  gencbvex  3520  clel5  3644  eqsbc2  3829  dfss  3945  sspsstri  4080  ssnelpss  4089  ssdifim  4248  disj  4425  disj4  4434  reuprg0  4678  preq1b  4822  invdisj  5105  disjprg  5115  dtruALT  5358  reusv3  5375  opthg2  5454  copsex2g  5468  copsex4g  5470  opcom  5476  opeqsng  5478  opeqpr  5480  snopeqop  5481  propeqop  5482  opthwiener  5489  vopelopabsb  5504  opthprc  5718  elxp3  5720  relop  5830  dmopab3  5899  rnopab3  5936  rncoeq  5959  restidsing  6040  somin1  6122  xpcan  6165  xpcan2  6166  dfrel4v  6179  dmsnn0  6196  reu3op  6281  reuop  6282  opreu2reurex  6283  ordtri2  6387  ordtri2or3  6453  suc11  6460  on0eqel  6477  snsn0non  6478  iota1  6507  iotan0  6520  sniota  6521  mptfnf  6672  fresaunres1  6750  dffn5  6936  fvelrnb  6938  dfimafn2  6941  funimass4  6942  feqmptdf  6948  fnsnfv  6957  dmfco  6974  fndmdif  7031  fneqeql  7035  rexrn  7076  ralrn  7077  elrnrexdmb  7079  dffo4  7092  fssrescdmd  7115  funopsn  7137  ftpg  7145  fprb  7185  ralima  7228  reximaOLD  7230  ralimaOLD  7231  fvclss  7232  dff13  7246  f1eqcocnv  7293  fnssintima  7354  imaeqsexvOLD  7355  riotaeqimp  7386  eusvobj2  7395  f1ocnvfv3  7398  oprabidw  7434  oprabid  7435  oprabv  7465  eloprabga  7514  ovelimab  7583  onmindif2  7799  br1steqg  8008  br2ndeqg  8009  dfoprab3  8051  opiota  8056  f1o2ndf1  8119  soseq  8156  brtpos2  8229  tpossym  8255  mpocurryd  8266  rdglim2  8444  tz7.48lem  8453  oaf1o  8573  omopthi  8671  erth2  8769  brecop  8822  erovlem  8825  ecopovsym  8831  eceqoveq  8834  xpcomco  9074  omxpenlem  9085  mapen  9153  nneneq  9218  unxpdomlem3  9258  unfilem1  9313  mapfien  9418  supgtoreq  9481  wemapsolem  9562  suc11reg  9631  inf3lem2  9641  inf3lem6  9645  ttrcltr  9728  djulf1o  9924  djurf1o  9925  infenaleph  10103  isinfcard  10104  dfac5  10141  cfeq0  10268  cfsuc  10269  ssfin4  10322  fin23lem25  10336  fin23lem22  10339  fin23lem40  10363  fin1a2lem5  10416  axcclem  10469  brdom7disj  10543  brdom6disj  10544  inar1  10787  psslinpr  11043  ltexprlem4  11051  ltsrpr  11089  mulgt0sr  11117  elreal  11143  ltresr  11152  leloe  11319  eqlei2  11344  addsubeq4  11495  subcan2  11506  negcon1  11533  negcon2  11534  addid0  11654  addeq0  11658  divmul2  11898  conjmul  11956  rereccl  11957  creur  12232  creui  12233  nndiv  12284  nn0sub  12549  elnn0z  12599  elznn0  12601  xrleloe  13158  ngtmnft  13180  icoshftf1o  13489  iccf1o  13511  fzen  13556  fzneuz  13623  injresinj  13802  fleqceilz  13869  mod0  13891  modmuladdnn0  13931  modirr  13958  addmodlteq  13962  nn0ennn  13995  hashrabsn01  14389  hashsdom  14397  hashgt12el2  14439  hashbclem  14468  hashfacen  14470  hashf1lem1  14471  hashtpg  14501  tpf1o  14517  fi1uzind  14523  ccatw2s1p1  14652  wrd2ind  14739  cshw1  14838  cshwsexa  14840  scshwfzeqfzo  14843  s2f1o  14933  wwlktovfo  14975  dmtrclfv  15035  cjreb  15140  leabs  15316  reusq0  15479  incexc2  15852  rpnnen2lem12  16241  dvdsval2  16273  dvdsabseq  16330  dvdsflip  16334  odd2np1  16358  oddm1even  16360  sqoddm1div8z  16371  m1exp1  16393  divalglem4  16413  divalglem8  16417  divalgb  16421  modremain  16425  zeqzmulgcd  16527  dfgcd2  16563  lcmfpr  16644  lcmftp  16653  lcmfunsnlem2  16657  divgcdcoprm0  16682  prm2orodd  16708  hashdvds  16792  oddprmdvds  16921  vdwlem12  17010  cshwshashlem1  17113  cshwsiun  17117  initoid  18012  termoid  18013  setcinv  18101  yonedainv  18291  joinfval  18381  joinfval2  18382  meetfval  18395  meetfval2  18396  latnle  18481  sgrp2nmndlem3  18901  grpid  18956  grpinvcnv  18987  grplmulf1o  18994  grpraddf1o  18995  grpsubeq0  19007  grpsubadd  19009  grplactcnv  19024  ressmulgnnd  19059  isnsg4  19148  eqg0el  19164  cycsubmel  19181  conjghm  19230  conjnmzb  19234  gacan  19286  gapm  19287  cntzrec  19317  oppgcntz  19345  fvcosymgeq  19408  odmulgeq  19536  dfod2  19543  sylow3lem3  19608  sylow3lem6  19611  lssnle  19653  lsmhash  19684  efgredlemb  19725  efgrelexlemb  19729  dprd2d2  20025  ablfac1eulem  20053  pgpfac1lem2  20056  pgpfac1lem4  20059  dvdsrval  20319  dvdsr02  20330  01eq0ring  20488  0ring01eqbi  20490  rngcinv  20595  ringcinv  20629  rmodislmodlem  20884  lvecinv  21072  rngqiprngimf1lem  21253  rspsn  21292  dfcnfldOLD  21329  prmirredlem  21431  zndvds  21508  znleval  21513  psrbagconf1o  21887  mplmonmul  21992  gsummoncoe1  22244  evl1maprhm  22315  mat1dimelbas  22407  mat1dimbas  22408  1mavmul  22484  ma1repveval  22507  mulmarep1gsum1  22509  mdetunilem9  22556  m2cpminvid2lem  22690  pmatcollpw3lem  22719  mp2pm2mplem4  22745  toponsspwpw  22858  dmtopon  22859  cmpfi  23344  ssref  23448  qtopeu  23652  hmeoimaf1o  23706  txhmeo  23739  fbasrn  23820  rnelfmlem  23888  hauspwpwf1  23923  alexsubALTlem4  23986  qustgpopn  24056  qustgphaus  24059  fmucndlem  24227  isngp3  24535  isngp4  24549  metnrmlem1a  24796  icopnfcnv  24889  iccpnfcnv  24891  ivthle  25407  ivthle2  25408  dyadmbl  25551  mbfinf  25616  i1fmulclem  25653  itg1mulc  25655  mvth  25947  dvivth  25965  lhop2  25970  r1pid2  26117  dvdsq1p  26118  reeff1o  26407  coseq1  26484  recosf1o  26494  resinf1o  26495  efopn  26617  cxpeq  26717  logreclem  26722  affineequiv  26783  affineequiv4  26786  affineequivne  26787  quad2  26799  dcubic  26806  mcubic  26807  quart  26821  atandm2  26837  rlimcnp2  26926  amgm  26951  wilthlem2  27029  mumullem2  27140  sqff1o  27142  dvdsflf1o  27147  gausslemma2dlem0i  27325  lgseisenlem2  27337  lgsquadlem2  27342  2lgslem1c  27354  2lgsoddprmlem2  27370  2lgsoddprm  27377  2sq2  27394  addsq2reu  27401  2sqreultlem  27408  2sqreunnltlem  27411  2sqreulem3  27414  sltval2  27618  sltintdifex  27623  sltres  27624  nosepon  27627  noextenddif  27630  nosepssdm  27648  nogt01o  27658  nosupprefixmo  27662  noinfprefixmo  27663  nosupno  27665  noinfno  27680  sleloe  27716  eqscut2  27768  scutbdaylt  27780  elold  27825  made0  27829  lrrecfr  27893  subadds  28017  cutpw2  28334  renegscl  28347  tgjustf  28398  legtrid  28516  legso  28524  islmib  28712  lmicom  28713  lmiinv  28717  lmimid  28719  lmiopp  28727  colinearalglem2  28832  colinearalg  28835  ax5seglem4  28857  ax5seglem5  28858  axlowdimlem13  28879  axeuclidlem  28887  axeuclid  28888  axcontlem2  28890  axcontlem4  28892  elntg2  28910  structiedg0val  28947  uspgredgiedg  29100  uspgriedgedg  29101  usgredgsscusgredg  29385  fusgrn0degnn0  29425  umgr2v2evtxel  29448  vdiscusgrb  29456  uspgr2wlkeq  29572  wlk0prc  29580  wlklenvclwlk  29581  wlkp1lem8  29606  spthdep  29662  usgr2pthlem  29691  usgr2pth  29692  wlkiswwlksupgr2  29805  wlklnwwlkln2lem  29810  wwlksnextproplem3  29839  umgr2adedgwlk  29873  umgr2adedgspth  29876  umgr2wlkon  29878  umgrwwlks2on  29885  elwwlks2  29894  elwspths2spth  29895  clwlkclwwlklem2a4  29924  clwlkclwwlklem2  29927  erclwwlkref  29947  clwwlkf  29974  erclwwlknref  29996  erclwwlknsym  29997  erclwwlkntr  29998  hashecclwwlkn1  30004  umgrhashecclwwlk  30005  eupth2lem2  30146  eucrct2eupth  30172  numclwwlkqhash  30302  isgrpo  30424  hvsubaddi  30993  hire  31021  shmodsi  31316  omlsilem  31329  chcon1i  31392  chnlei  31412  pjoml3i  31513  cmbr2i  31523  chscllem2  31565  adjsym  31760  eigorthi  31764  dfadj2  31812  adjval2  31818  cnvadj  31819  dmadjrnb  31833  adjvalval  31864  cnlnadjeui  32004  cnlnssadj  32007  adjbdln  32010  pjimai  32103  pjin2i  32120  pjin3i  32121  stadd3i  32175  largei  32194  cvnbtwn3  32215  cvnbtwn4  32216  mddmd2  32236  superpos  32281  atnemeq0  32304  sumdmdii  32342  sumdmdlem  32345  addltmulALT  32373  opreu2reuALT  32404  foresf1o  32431  difeq  32445  disjrdx  32518  fcoinvbr  32532  brab2d  32533  fmptco1f1o  32557  dfimafnf  32560  funcnvmpt  32591  curry2ima  32632  intimafv  32634  receqid  32668  elicoelioo  32701  fzo0opth  32728  ind1a  32782  wrdt2ind  32875  swrdrn3  32877  orngsqr  33272  qusker  33310  dvdsrspss  33348  lsmsnorb  33352  1arithufdlem4  33508  r1pid2OLD  33564  algextdeglem8  33704  zarcls  33851  xrmulc1cn  33907  xrge0iifcnv  33910  esumfsup  34047  esumpcvgval  34055  esumcvg  34063  esum2dlem  34069  issgon  34100  eulerpartgbij  34350  eulerpartlemgh  34356  ballotlemsima  34494  bnj1366  34806  bnj553  34875  bnj964  34920  cusgredgex  35090  revwlk  35093  loop1cycl  35105  subfacp1lem3  35150  subfacp1lem5  35152  erdszelem9  35167  prv1n  35399  ply1divalg3  35610  quad3  35638  br6  35720  elintfv  35728  dfon2lem5  35751  dfon2lem8  35754  brbigcup  35862  dfbigcup2  35863  elfix  35867  ellimits  35874  snelsingles  35886  dfiota3  35887  imageval  35894  brapply  35902  brsuccf  35905  funpartlem  35906  brfullfun  35912  dfrecs2  35914  dfrdg4  35915  altopthbg  35932  altopthc  35935  altopthd  35936  altopelaltxp  35940  brsegle  36072  outsideofrflx  36091  elicc3  36281  nn0prpw  36287  opnregcld  36294  cldregopn  36295  fneval  36316  topfneec  36319  knoppndvlem9  36484  bj-elgab  36903  bj-gabima  36904  bj-elsngl  36932  bj-snglc  36933  bj-projval  36960  bj-disj2r  36992  bj-restreg  37063  bj-0int  37065  copsex2b  37104  bj-inftyexpitaudisj  37169  bj-inftyexpidisj  37174  bj-bary1lem1  37275  topdifinffinlem  37311  topdifinfeq  37314  fvineqsnf1  37374  curf  37568  uncf  37569  curunc  37572  unccur  37573  poimirlem2  37592  poimirlem16  37606  poimirlem17  37607  poimirlem19  37609  poimirlem20  37610  poimirlem27  37617  mblfinlem2  37628  mbfresfi  37636  itg2addnclem2  37642  ftc1anclem3  37665  fdc  37715  heibor1  37780  opidonOLD  37822  0rngo  37997  smprngopr  38022  isfldidl  38038  isfldidl2  38039  eqbrb  38197  eqelb  38199  ideq2  38271  relcnveq  38286  n0elqs  38290  disjressuc2  38352  elrelscnveq  38456  disjdmqscossss  38767  lcvnbtwn3  38992  lcvexchlem1  38998  lsatnem0  39009  opcon1b  39162  omllaw2N  39208  cmtbr2N  39217  leatb  39256  cvlsupr2  39307  glbconxN  39343  islln3  39475  llnexatN  39486  islpln3  39498  lplnexatN  39528  islvol3  39541  dalem-cly  39636  isline4N  39742  2llnma3r  39753  poml4N  39918  4atex2  40042  4atex2-0bOLDN  40044  cdlemefrs29bpre0  40361  cdlemftr3  40530  cdlemb3  40571  cdlemg17h  40633  cdlemg17pq  40637  cdlemg19  40649  cdlemg21  40651  tendoex  40940  dva1dim  40950  dihglb2  41307  doch11  41338  dochsordN  41339  lcfrlem9  41515  hlhillcs  41923  lcmineqlem4  41991  aks6d1c7lem2  42140  aks5lem3a  42148  aks5lem6  42151  unitscyglem2  42155  unitscyglem3  42156  metakunt1  42164  metakunt6  42169  metakunt15  42178  metakunt16  42179  addsubeq4com  42277  ef11d  42335  fimgmcyclem  42503  fsuppind  42560  elrfirn  42665  isnacs2  42676  isnacs3  42680  fiphp3d  42789  wopprc  43001  islnm2  43049  kercvrlsm  43054  fgraphopab  43174  tfsconcatlem  43307  tfsconcatrn  43313  tfsconcat0i  43316  tfsconcat0b  43317  tfsconcatrev  43319  oaun3lem1  43345  oadif1lem  43350  oadif1  43351  rp-fakeuninass  43487  snen1g  43495  iscard4  43504  sqrtcval  43612  frege124d  43732  frege129d  43734  frege92  43926  dffrege99  43933  clsk3nimkb  44011  clsk1indlem4  44015  clsk1indlem1  44016  ntrclsiso  44038  ntrclsk3  44041  ntrclsk13  44042  ntrneik4w  44071  extoimad  44135  int-sqdefd  44152  int-sqgeq0d  44157  radcnvrat  44286  bcc0  44312  opelopab4  44524  eqsbc2VD  44812  fzisoeu  45277  iuneqfzuz  45310  supxrleubrnmptf  45426  rexanuz2nf  45467  fsummulc1f  45548  fsumiunss  45552  fmul01lt1lem2  45562  sumnnodd  45607  fnlimfvre2  45654  limsupreuz  45714  limsupvaluz2  45715  liminfvalxr  45760  icccncfext  45864  cncfiooicc  45871  cncfioobdlem  45873  dvmptmulf  45914  dvmptfprodlem  45921  volioc  45949  itgioocnicc  45954  fourierdlem12  46096  fourierdlem20  46104  fourierdlem25  46109  fourierdlem33  46117  fourierdlem42  46126  fourierdlem52  46135  fourierdlem54  46137  fourierdlem57  46140  fourierdlem58  46141  fourierdlem59  46142  fourierdlem63  46146  fourierdlem65  46148  fourierdlem68  46151  fourierdlem73  46156  fourierdlem74  46157  fourierdlem75  46158  fourierdlem80  46163  fourierdlem81  46164  rrndistlt  46267  sge0ltfirpmpt2  46403  sge0pnfmpt  46422  hoidmv1le  46571  hoidmvle  46577  vonioolem2  46658  smflimlem3  46750  lambert0  46867  lamberte  46868  euabsneu  47005  funressnfv  47020  aiotaval  47072  reuf1odnf  47084  reuf1od  47085  afvpcfv0  47123  dfafn5a  47137  afvelrnb  47140  afvelrnb0  47141  dfaimafn2  47143  dfatsnafv2  47229  dfatdmfcoafv2  47231  f1oresf1o2  47268  ceilbi  47310  minusmodnep2tmod  47330  0nelsetpreimafv  47352  fargshiftfo  47404  sprsymrelf1  47458  reupr  47484  fmtnorec2lem  47504  fmtnoprmfac1  47527  fmtnoprmfac2  47529  sfprmdvdsmersenne  47565  lighneallem2  47568  dfeven2  47611  dfodd3  47612  odd2np1ALTV  47636  even3prm2  47681  fppr2odd  47693  nnsum3primesgbe  47754  nnsum3primesle9  47756  clnbgrsym  47799  dfvopnbgr2  47814  isuspgrim0  47855  isuspgrimlem  47856  dfgric2  47876  grtriprop  47901  uspgrlimlem3  47950  gpgvtxedg1  48016  0nodd  48093  2nodd  48095  lmod0rng  48152  rngcinvALTV  48199  ringcinvALTV  48233  lcoel0  48352  lindslinindimp2lem4  48385  ldepspr  48397  lincresunit3  48405  nn0sumshdiglemB  48548  nn0sumshdiglem1  48549  rrx2pnedifcoorneorr  48645  eenglngeehlnmlem1  48665  eenglngeehlnmlem2  48666  rrx2linest  48670  rrx2linest2  48672  rrxsphere  48676  line2ylem  48679  line2x  48682  itscnhlc0xyqsol  48693  itschlc0xyqsol1  48694  itsclinecirc0b  48702  2itscp  48709  inlinecirc02plem  48714  brab2dd  48754