Theorem eqcom 2804

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

Syntax hints:   ↔ wb 207   = wceq 1525

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1781  ax-4 1795  ax-5 1892  ax-6 1951  ax-7 1996  ax-9 2093  ax-ext 2771

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1766  df-cleq 2790

This theorem is referenced by:  eqcoms  2805  eqcomi  2806  eqeq2d  2807  eqtr2  2819  eqtr3  2820  abeq1  2917  necom  3039  nesym  3042  pm13.181  3069  gencbvex  3495  clel5  3598  eqsbc3r  3771  dfss  3881  sspsstri  4006  ssnelpss  4015  ssdifim  4165  disj4  4328  reuprg0  4551  preq1b  4690  invdisj  4954  disjprg  4964  dtruALT  5186  reusv3  5204  dtruALT2  5234  opthg2  5270  copsex4g  5283  opcom  5289  opeqsng  5291  opeqpr  5293  snopeqop  5294  propeqop  5295  opthwiener  5302  opthprc  5509  elxp3  5511  relop  5614  dmopab3  5681  rncoeq  5734  restidsing  5807  somin1  5876  xpcan  5916  xpcan2  5917  dfrel4v  5930  dmsnn0  5946  reu3op  6025  reuop  6026  opreu2reurex  6027  ordtri2  6108  ordtri2or3  6170  suc11  6176  on0eqel  6190  snsn0non  6191  iota1  6210  sniota  6223  mptfnf  6358  fresaunres1  6426  dffn5  6599  fvelrnb  6601  dfimafn2  6604  funimass4  6605  feqmptdf  6610  fnsnfv  6617  dmfco  6631  fndmdif  6684  fneqeql  6688  rexrn  6725  ralrn  6726  elrnrexdmb  6728  dffo4  6739  funopsn  6780  ftpg  6788  fprb  6830  rexima  6871  ralima  6872  fvclss  6873  dff13  6885  f1eqcocnv  6929  riotaeqimp  7007  eusvobj2  7016  f1ocnvfv3  7019  oprabid  7054  oprabv  7080  eloprabga  7124  ovelimab  7189  onmindif2  7390  br1steqg  7574  br2ndeqg  7575  dfoprab3  7615  opiota  7620  f1o2ndf1  7678  brtpos2  7756  tpossym  7782  mpocurryd  7793  rdglim2  7927  tz7.48lem  7935  oaf1o  8046  omopthi  8141  erth2  8196  brecop  8247  erovlem  8250  ecopovsym  8256  eceqoveq  8259  xpcomco  8461  omxpenlem  8472  mapen  8535  nneneq  8554  unxpdomlem3  8577  unfilem1  8635  mapfien  8724  supgtoreq  8787  wemapsolem  8867  suc11reg  8935  inf3lem2  8945  inf3lem6  8949  djulf1o  9194  djurf1o  9195  infenaleph  9370  isinfcard  9371  dfac5  9407  cfeq0  9531  cfsuc  9532  ssfin4  9585  fin23lem25  9599  fin23lem22  9602  fin23lem40  9626  fin1a2lem5  9679  axcclem  9732  brdom7disj  9806  brdom6disj  9807  inar1  10050  psslinpr  10306  ltexprlem4  10314  ltsrpr  10352  mulgt0sr  10380  elreal  10406  ltresr  10415  leloe  10580  eqlei2  10604  addsubeq4  10755  subcan2  10765  negcon1  10792  negcon2  10793  addid0  10913  addeq0  10917  divmul2  11156  conjmul  11211  rereccl  11212  creur  11486  creui  11487  nndiv  11537  nn0sub  11801  elnn0z  11848  elznn0  11850  zqOLD  12208  xrleloe  12391  ngtmnft  12413  icoshftf1o  12714  iccf1o  12736  fzen  12778  fzneuz  12842  injresinj  13012  fleqceilz  13076  mod0  13098  modmuladdnn0  13137  modirr  13164  addmodlteq  13168  nn0ennn  13201  hashrabsn01  13586  hashsdom  13594  hashgt12el2  13636  hashbclem  13662  hashfacen  13664  hashf1lem1  13665  hashtpg  13693  fi1uzind  13705  ccatw2s1p1  13838  wrd2ind  13925  cshwlen  14001  cshw1  14024  scshwfzeqfzo  14028  s2f1o  14118  wwlktovfo  14160  dmtrclfv  14216  cjreb  14320  leabs  14497  reusq0  14660  incexc2  15030  pwm1geoserOLD  15062  rpnnen2lem12  15415  dvdsval2  15447  dvdsabseq  15500  dvdsflip  15504  odd2np1  15527  oddm1even  15529  sqoddm1div8z  15540  m1exp1  15564  divalglem4  15584  divalglem8  15588  divalgb  15592  modremain  15596  zeqzmulgcd  15696  dfgcd2  15727  lcmfpr  15804  lcmftp  15813  lcmfunsnlem2  15817  divgcdcoprm0  15842  prm2orodd  15868  hashdvds  15945  oddprmdvds  16072  vdwlem12  16161  cshwshashlem1  16262  cshwsiun  16266  initoid  17098  termoid  17099  setcinv  17183  yonedainv  17364  joinfval  17444  joinfval2  17445  meetfval  17458  meetfval2  17459  latnle  17528  sgrp2nmndlem3  17855  grpid  17900  grpinvcnv  17928  grplmulf1o  17934  grpsubeq0  17946  grpsubadd  17948  grplactcnv  17963  isnsg4  18080  conjghm  18134  conjnmzb  18138  gacan  18180  gapm  18181  cntzrec  18209  oppgcntz  18237  fvcosymgeq  18292  odmulgeq  18418  dfod2  18425  sylow3lem3  18488  sylow3lem6  18491  lssnle  18531  lsmhash  18562  efgredlemb  18603  efgrelexlemb  18607  dprd2d2  18887  ablfac1eulem  18915  pgpfac1lem2  18918  pgpfac1lem4  18921  dvdsrval  19089  dvdsr02  19100  rmodislmodlem  19395  lvecinv  19579  rspsn  19720  0ring01eqbi  19739  psrbagconf1o  19846  mplmonmul  19936  gsummoncoe1  20159  prmirredlem  20326  zndvds  20382  znleval  20387  mat1dimelbas  20768  mat1dimbas  20769  1mavmul  20845  ma1repveval  20868  mulmarep1gsum1  20870  mdetunilem9  20917  m2cpminvid2lem  21050  pmatcollpw3lem  21079  mp2pm2mplem4  21105  toponsspwpw  21218  dmtopon  21219  cmpfi  21704  ssref  21808  qtopeu  22012  hmeoimaf1o  22066  txhmeo  22099  fbasrn  22180  rnelfmlem  22248  hauspwpwf1  22283  alexsubALTlem4  22346  qustgpopn  22415  qustgphaus  22418  fmucndlem  22587  isngp3  22894  isngp4  22908  metnrmlem1a  23153  icopnfcnv  23233  iccpnfcnv  23235  ivthle  23744  ivthle2  23745  dyadmbl  23888  mbfinf  23953  i1fmulclem  23990  itg1mulc  23992  mvth  24276  dvivth  24294  lhop2  24299  dvdsq1p  24441  reeff1o  24722  coseq1  24797  recosf1o  24804  resinf1o  24805  efopn  24926  cxpeq  25023  logreclem  25025  affineequiv  25086  affineequiv4  25089  affineequivne  25090  quad2  25102  dcubic  25109  mcubic  25110  quart  25124  atandm2  25140  rlimcnp2  25230  amgm  25254  wilthlem2  25332  mumullem2  25443  sqff1o  25445  dvdsflf1o  25450  gausslemma2dlem0i  25626  lgseisenlem2  25638  lgsquadlem2  25643  2lgslem1c  25655  2lgsoddprmlem2  25671  2lgsoddprm  25678  2sq2  25695  addsq2reu  25702  2sqreultlem  25709  2sqreunnltlem  25712  2sqreulem3  25715  tgjustf  25945  legtrid  26063  legso  26071  islmib  26259  lmicom  26260  lmiinv  26264  lmimid  26266  lmiopp  26274  colinearalglem2  26380  colinearalg  26383  ax5seglem4  26405  ax5seglem5  26406  axlowdimlem13  26427  axeuclidlem  26435  axeuclid  26436  axcontlem2  26438  axcontlem4  26440  elntg2  26458  structiedg0val  26494  usgredgsscusgredg  26928  fusgrn0degnn0  26968  umgr2v2evtxel  26991  vdiscusgrb  26999  uspgr2wlkeq  27114  wlk0prc  27122  wlklenvclwlk  27123  wlkp1lem8  27148  spthdep  27201  usgr2pthlem  27230  usgr2pth  27231  wlkiswwlksupgr2  27341  wlklnwwlkln2lem  27346  wwlksnextproplem3  27376  umgr2adedgwlk  27410  umgr2adedgspth  27413  umgr2wlkon  27415  umgrwwlks2on  27422  elwwlks2  27431  elwspths2spth  27432  clwlkclwwlklem2a4  27461  clwlkclwwlklem2  27464  erclwwlkref  27484  clwwlkf  27512  erclwwlknref  27534  erclwwlknsym  27535  erclwwlkntr  27536  hashecclwwlkn1  27542  umgrhashecclwwlk  27543  eupth2lem2  27684  eucrct2eupth  27710  numclwwlkqhash  27842  isgrpo  27961  hvsubaddi  28530  hire  28558  shmodsi  28853  omlsilem  28866  chcon1i  28929  chnlei  28949  pjoml3i  29050  cmbr2i  29060  chscllem2  29102  adjsym  29297  eigorthi  29301  dfadj2  29349  adjval2  29355  cnvadj  29356  dmadjrnb  29370  adjvalval  29401  cnlnadjeui  29541  cnlnssadj  29544  adjbdln  29547  pjimai  29640  pjin2i  29657  pjin3i  29658  stadd3i  29712  largei  29731  cvnbtwn3  29752  cvnbtwn4  29753  mddmd2  29773  superpos  29818  atnemeq0  29841  sumdmdii  29879  sumdmdlem  29882  addltmulALT  29910  opreu2reuALT  29928  foresf1o  29953  difeq  29965  disjrdx  30027  fcoinvbr  30044  fmptco1f1o  30064  dfimafnf  30067  funcnvmpt  30098  curry2ima  30128  cnvoprabOLD  30140  elicoelioo  30185  wrdt2ind  30302  orngsqr  30527  qusker  30568  xrmulc1cn  30786  xrge0iifcnv  30789  ind1a  30891  esumfsup  30942  esumpcvgval  30950  esumcvg  30958  esum2dlem  30964  issgon  30995  eulerpartgbij  31243  eulerpartlemgh  31249  ballotlemsima  31386  bnj1366  31714  bnj553  31782  bnj964  31827  cusgredgex  31978  revwlk  31981  loop1cycl  31994  subfacp1lem3  32039  subfacp1lem5  32041  erdszelem9  32056  prv1n  32288  quad3  32523  br6  32603  elintfv  32617  dfon2lem5  32642  dfon2lem8  32645  soseq  32707  sltval2  32774  sltintdifex  32779  sltres  32780  nosepon  32783  noextenddif  32786  nosepssdm  32801  nosupno  32814  sleloe  32844  scutbdaylt  32887  brbigcup  32970  dfbigcup2  32971  elfix  32975  ellimits  32982  snelsingles  32994  dfiota3  32995  imageval  33002  brapply  33010  brsuccf  33013  funpartlem  33014  brfullfun  33020  dfrecs2  33022  dfrdg4  33023  altopthbg  33040  altopthc  33043  altopthd  33044  altopelaltxp  33048  brsegle  33180  outsideofrflx  33199  elicc3  33276  nn0prpw  33282  opnregcld  33289  cldregopn  33290  fneval  33311  topfneec  33314  knoppndvlem9  33470  bj-abeq1  33697  bj-elsngl  33906  bj-snglc  33907  bj-projval  33934  bj-disj2r  33963  bj-restreg  34010  bj-0int  34013  bj-inftyexpitaudisj  34066  bj-inftyexpidisj  34071  bj-bary1lem1  34150  topdifinffinlem  34180  topdifinfeq  34183  fvineqsnf1  34243  curf  34422  uncf  34423  curunc  34426  unccur  34427  poimirlem2  34446  poimirlem16  34460  poimirlem17  34461  poimirlem19  34463  poimirlem20  34464  poimirlem27  34471  mblfinlem2  34482  mbfresfi  34490  itg2addnclem2  34496  ftc1anclem3  34521  fdc  34573  heibor1  34641  opidonOLD  34683  0rngo  34858  smprngopr  34883  isfldidl  34899  isfldidl2  34900  eqelb  35055  ideq2  35118  relcnveq  35132  n0elqs  35136  elrelscnveq  35284  lcvnbtwn3  35716  lcvexchlem1  35722  lsatnem0  35733  opcon1b  35886  omllaw2N  35932  cmtbr2N  35941  leatb  35980  cvlsupr2  36031  glbconxN  36066  islln3  36198  llnexatN  36209  islpln3  36221  lplnexatN  36251  islvol3  36264  dalem-cly  36359  isline4N  36465  2llnma3r  36476  poml4N  36641  4atex2  36765  4atex2-0bOLDN  36767  cdlemefrs29bpre0  37084  cdlemftr3  37253  cdlemb3  37294  cdlemg17h  37356  cdlemg17pq  37360  cdlemg19  37372  cdlemg21  37374  tendoex  37663  dva1dim  37673  dihglb2  38030  doch11  38061  dochsordN  38062  lcfrlem9  38238  hlhillcs  38646  addsubeq4com  38709  elrfirn  38798  isnacs2  38809  isnacs3  38813  fiphp3d  38922  wopprc  39133  islnm2  39184  kercvrlsm  39189  fgraphopab  39316  rp-fakeuninass  39388  snen1g  39396  iscard4  39406  frege124d  39612  frege129d  39614  frege92  39807  dffrege99  39814  clsk3nimkb  39896  clsk1indlem4  39900  clsk1indlem1  39901  ntrclsiso  39923  ntrclsk3  39926  ntrclsk13  39927  ntrneik4w  39956  extoimad  40021  int-sqdefd  40041  int-sqgeq0d  40046  neqcomd  40064  radcnvrat  40205  bcc0  40231  opelopab4  40445  eqsbc3rVD  40734  fzisoeu  41129  iuneqfzuz  41165  supxrleubrnmptf  41290  fsummulc1f  41414  fsumiunss  41419  fmul01lt1lem2  41429  sumnnodd  41474  fnlimfvre2  41521  limsupreuz  41581  limsupvaluz2  41582  liminfvalxr  41627  icccncfext  41733  cncfiooicc  41740  cncfioobdlem  41742  dvmptmulf  41785  dvmptfprodlem  41792  volioc  41820  itgioocnicc  41825  fourierdlem12  41968  fourierdlem20  41976  fourierdlem25  41981  fourierdlem33  41989  fourierdlem42  41998  fourierdlem52  42007  fourierdlem54  42009  fourierdlem57  42012  fourierdlem58  42013  fourierdlem59  42014  fourierdlem63  42018  fourierdlem65  42020  fourierdlem68  42023  fourierdlem73  42028  fourierdlem74  42029  fourierdlem75  42030  fourierdlem80  42035  fourierdlem81  42036  rrndistlt  42139  sge0ltfirpmpt2  42272  sge0pnfmpt  42291  hoidmv1le  42440  hoidmvle  42446  vonioolem2  42527  smflimlem3  42613  euabsneu  42801  funressnfv  42816  aiotaval  42831  reuf1odnf  42844  reuf1od  42845  afvpcfv0  42883  dfafn5a  42897  afvelrnb  42900  afvelrnb0  42901  dfaimafn2  42903  dfatsnafv2  42989  dfatdmfcoafv2  42991  f1oresf1o2  43028  fargshiftfo  43106  sprsymrelf1  43162  reupr  43188  fmtnorec2lem  43208  fmtnoprmfac1  43231  fmtnoprmfac2  43233  sfprmdvdsmersenne  43272  lighneallem2  43275  dfeven2  43318  dfodd3  43319  odd2np1ALTV  43343  even3prm2  43388  fppr2odd  43400  nnsum3primesgbe  43461  nnsum3primesle9  43463  isomuspgrlem2d  43500  0nodd  43581  2nodd  43583  lmod0rng  43639  rngcinv  43752  rngcinvALTV  43764  ringcinv  43803  ringcinvALTV  43827  lcoel0  43985  lindslinindimp2lem4  44018  ldepspr  44030  lincresunit3  44038  nn0sumshdiglemB  44183  nn0sumshdiglem1  44184  rrx2pnedifcoorneorr  44207  eenglngeehlnmlem1  44227  eenglngeehlnmlem2  44228  rrx2linest  44232  rrx2linest2  44234  rrxsphere  44238  line2ylem  44241  line2x  44244  itscnhlc0xyqsol  44255  itschlc0xyqsol1  44256  itsclinecirc0b  44264  2itscp  44271  inlinecirc02plem  44276