Theorem eqcom 2737

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 2736	. 2 ⊢ (𝐴 = 𝐵 → 𝐵 = 𝐴)
3		id 22	. . 3 ⊢ (𝐵 = 𝐴 → 𝐵 = 𝐴)
4	3	eqcomd 2736	. 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 2008  ax-9 2119  ax-ext 2702

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

This theorem is referenced by:  eqcoms  2738  eqcomi  2739  neqcomd  2740  eqeq2d  2741  eqabcb  2870  necom  2979  nesym  2982  gencbvex  3510  clel5  3634  eqsbc2  3820  dfss  3936  sspsstri  4071  ssnelpss  4080  ssdifim  4239  disj  4416  disj4  4425  reuprg0  4669  preq1b  4813  invdisj  5096  disjprg  5106  dtruALT  5346  reusv3  5363  opthg2  5442  copsex2g  5456  copsex4g  5458  opcom  5464  opeqsng  5466  opeqpr  5468  snopeqop  5469  propeqop  5470  opthwiener  5477  vopelopabsb  5492  opthprc  5705  elxp3  5707  relop  5817  dmopab3  5886  rnopab3  5923  rncoeq  5946  restidsing  6027  somin1  6109  xpcan  6152  xpcan2  6153  dfrel4v  6166  dmsnn0  6183  reu3op  6268  reuop  6269  opreu2reurex  6270  ordtri2  6370  ordtri2or3  6437  suc11  6444  on0eqel  6461  snsn0non  6462  iota1  6491  iotan0  6504  sniota  6505  mptfnf  6656  fresaunres1  6736  dffn5  6922  fvelrnb  6924  dfimafn2  6927  funimass4  6928  feqmptdf  6934  fnsnfv  6943  dmfco  6960  fndmdif  7017  fneqeql  7021  rexrn  7062  ralrn  7063  elrnrexdmb  7065  dffo4  7078  fssrescdmd  7101  funopsn  7123  ftpg  7131  fprb  7171  ralima  7214  reximaOLD  7216  ralimaOLD  7217  fvclss  7218  dff13  7232  f1eqcocnv  7279  fnssintima  7340  imaeqsexvOLD  7341  riotaeqimp  7373  eusvobj2  7382  f1ocnvfv3  7385  oprabidw  7421  oprabid  7422  oprabv  7452  eloprabga  7501  ovelimab  7570  onmindif2  7786  br1steqg  7993  br2ndeqg  7994  dfoprab3  8036  opiota  8041  f1o2ndf1  8104  soseq  8141  brtpos2  8214  tpossym  8240  mpocurryd  8251  rdglim2  8403  tz7.48lem  8412  oaf1o  8530  omopthi  8628  erth2  8729  brecop  8786  erovlem  8789  ecopovsym  8795  eceqoveq  8798  xpcomco  9036  omxpenlem  9047  mapen  9111  nneneq  9176  unxpdomlem3  9206  unfilem1  9261  mapfien  9366  supgtoreq  9429  wemapsolem  9510  suc11reg  9579  inf3lem2  9589  inf3lem6  9593  ttrcltr  9676  djulf1o  9872  djurf1o  9873  infenaleph  10051  isinfcard  10052  dfac5  10089  cfeq0  10216  cfsuc  10217  ssfin4  10270  fin23lem25  10284  fin23lem22  10287  fin23lem40  10311  fin1a2lem5  10364  axcclem  10417  brdom7disj  10491  brdom6disj  10492  inar1  10735  psslinpr  10991  ltexprlem4  10999  ltsrpr  11037  mulgt0sr  11065  elreal  11091  ltresr  11100  leloe  11267  eqlei2  11292  addsubeq4  11443  subcan2  11454  negcon1  11481  negcon2  11482  addid0  11604  addeq0  11608  divmul2  11848  conjmul  11906  rereccl  11907  creur  12187  creui  12188  nndiv  12239  nn0sub  12499  elnn0z  12549  elznn0  12551  xrleloe  13111  ngtmnft  13133  icoshftf1o  13442  iccf1o  13464  fzen  13509  fzneuz  13576  injresinj  13756  fleqceilz  13823  mod0  13845  modmuladdnn0  13887  modirr  13914  addmodlteq  13918  nn0ennn  13951  hashrabsn01  14345  hashsdom  14353  hashgt12el2  14395  hashbclem  14424  hashfacen  14426  hashf1lem1  14427  hashtpg  14457  tpf1o  14473  fi1uzind  14479  ccatw2s1p1  14608  wrd2ind  14695  cshw1  14794  cshwsexa  14796  scshwfzeqfzo  14799  s2f1o  14889  wwlktovfo  14931  dmtrclfv  14991  cjreb  15096  leabs  15272  reusq0  15438  incexc2  15811  rpnnen2lem12  16200  dvdsval2  16232  dvdsabseq  16290  dvdsflip  16294  odd2np1  16318  oddm1even  16320  sqoddm1div8z  16331  m1exp1  16353  divalglem4  16373  divalglem8  16377  divalgb  16381  modremain  16385  zeqzmulgcd  16487  dfgcd2  16523  lcmfpr  16604  lcmftp  16613  lcmfunsnlem2  16617  divgcdcoprm0  16642  prm2orodd  16668  hashdvds  16752  oddprmdvds  16881  vdwlem12  16970  cshwshashlem1  17073  cshwsiun  17077  initoid  17970  termoid  17971  setcinv  18059  yonedainv  18249  joinfval  18339  joinfval2  18340  meetfval  18353  meetfval2  18354  latnle  18439  sgrp2nmndlem3  18859  grpid  18914  grpinvcnv  18945  grplmulf1o  18952  grpraddf1o  18953  grpsubeq0  18965  grpsubadd  18967  grplactcnv  18982  ressmulgnnd  19017  isnsg4  19106  eqg0el  19122  cycsubmel  19139  conjghm  19188  conjnmzb  19192  gacan  19244  gapm  19245  cntzrec  19275  oppgcntz  19303  fvcosymgeq  19366  odmulgeq  19494  dfod2  19501  sylow3lem3  19566  sylow3lem6  19569  lssnle  19611  lsmhash  19642  efgredlemb  19683  efgrelexlemb  19687  dprd2d2  19983  ablfac1eulem  20011  pgpfac1lem2  20014  pgpfac1lem4  20017  dvdsrval  20277  dvdsr02  20288  01eq0ring  20446  0ring01eqbi  20448  rngcinv  20553  ringcinv  20587  rmodislmodlem  20842  lvecinv  21030  rngqiprngimf1lem  21211  rspsn  21250  dfcnfldOLD  21287  prmirredlem  21389  zndvds  21466  znleval  21471  psrbagconf1o  21845  mplmonmul  21950  gsummoncoe1  22202  evl1maprhm  22273  mat1dimelbas  22365  mat1dimbas  22366  1mavmul  22442  ma1repveval  22465  mulmarep1gsum1  22467  mdetunilem9  22514  m2cpminvid2lem  22648  pmatcollpw3lem  22677  mp2pm2mplem4  22703  toponsspwpw  22816  dmtopon  22817  cmpfi  23302  ssref  23406  qtopeu  23610  hmeoimaf1o  23664  txhmeo  23697  fbasrn  23778  rnelfmlem  23846  hauspwpwf1  23881  alexsubALTlem4  23944  qustgpopn  24014  qustgphaus  24017  fmucndlem  24185  isngp3  24493  isngp4  24507  metnrmlem1a  24754  icopnfcnv  24847  iccpnfcnv  24849  ivthle  25364  ivthle2  25365  dyadmbl  25508  mbfinf  25573  i1fmulclem  25610  itg1mulc  25612  mvth  25904  dvivth  25922  lhop2  25927  r1pid2  26074  dvdsq1p  26075  reeff1o  26364  coseq1  26441  recosf1o  26451  resinf1o  26452  efopn  26574  cxpeq  26674  logreclem  26679  affineequiv  26740  affineequiv4  26743  affineequivne  26744  quad2  26756  dcubic  26763  mcubic  26764  quart  26778  atandm2  26794  rlimcnp2  26883  amgm  26908  wilthlem2  26986  mumullem2  27097  sqff1o  27099  dvdsflf1o  27104  gausslemma2dlem0i  27282  lgseisenlem2  27294  lgsquadlem2  27299  2lgslem1c  27311  2lgsoddprmlem2  27327  2lgsoddprm  27334  2sq2  27351  addsq2reu  27358  2sqreultlem  27365  2sqreunnltlem  27368  2sqreulem3  27371  sltval2  27575  sltintdifex  27580  sltres  27581  nosepon  27584  noextenddif  27587  nosepssdm  27605  nogt01o  27615  nosupprefixmo  27619  noinfprefixmo  27620  nosupno  27622  noinfno  27637  sleloe  27673  eqscut2  27725  scutbdaylt  27737  elold  27788  made0  27792  lrrecfr  27857  subadds  27981  onscutlt  28172  zs12ge0  28349  renegscl  28356  tgjustf  28407  legtrid  28525  legso  28533  islmib  28721  lmicom  28722  lmiinv  28726  lmimid  28728  lmiopp  28736  colinearalglem2  28841  colinearalg  28844  ax5seglem4  28866  ax5seglem5  28867  axlowdimlem13  28888  axeuclidlem  28896  axeuclid  28897  axcontlem2  28899  axcontlem4  28901  elntg2  28919  structiedg0val  28956  uspgredgiedg  29109  uspgriedgedg  29110  usgredgsscusgredg  29394  fusgrn0degnn0  29434  umgr2v2evtxel  29457  vdiscusgrb  29465  uspgr2wlkeq  29581  wlk0prc  29589  wlklenvclwlk  29590  wlkp1lem8  29615  spthdep  29671  usgr2pthlem  29700  usgr2pth  29701  wlkiswwlksupgr2  29814  wlklnwwlkln2lem  29819  wwlksnextproplem3  29848  umgr2adedgwlk  29882  umgr2adedgspth  29885  umgr2wlkon  29887  umgrwwlks2on  29894  elwwlks2  29903  elwspths2spth  29904  clwlkclwwlklem2a4  29933  clwlkclwwlklem2  29936  erclwwlkref  29956  clwwlkf  29983  erclwwlknref  30005  erclwwlknsym  30006  erclwwlkntr  30007  hashecclwwlkn1  30013  umgrhashecclwwlk  30014  eupth2lem2  30155  eucrct2eupth  30181  numclwwlkqhash  30311  isgrpo  30433  hvsubaddi  31002  hire  31030  shmodsi  31325  omlsilem  31338  chcon1i  31401  chnlei  31421  pjoml3i  31522  cmbr2i  31532  chscllem2  31574  adjsym  31769  eigorthi  31773  dfadj2  31821  adjval2  31827  cnvadj  31828  dmadjrnb  31842  adjvalval  31873  cnlnadjeui  32013  cnlnssadj  32016  adjbdln  32019  pjimai  32112  pjin2i  32129  pjin3i  32130  stadd3i  32184  largei  32203  cvnbtwn3  32224  cvnbtwn4  32225  mddmd2  32245  superpos  32290  atnemeq0  32313  sumdmdii  32351  sumdmdlem  32354  addltmulALT  32382  opreu2reuALT  32413  foresf1o  32440  difeq  32454  disjrdx  32527  fcoinvbr  32541  brab2d  32542  fmptco1f1o  32564  dfimafnf  32567  funcnvmpt  32598  curry2ima  32639  intimafv  32641  receqid  32675  elicoelioo  32708  fzo0opth  32735  ind1a  32789  wrdt2ind  32882  swrdrn3  32884  cntrval2  33135  orngsqr  33289  qusker  33327  dvdsrspss  33365  lsmsnorb  33369  1arithufdlem4  33525  r1pid2OLD  33581  algextdeglem8  33721  zarcls  33871  xrmulc1cn  33927  xrge0iifcnv  33930  esumfsup  34067  esumpcvgval  34075  esumcvg  34083  esum2dlem  34089  issgon  34120  eulerpartgbij  34370  eulerpartlemgh  34376  ballotlemsima  34514  bnj1366  34826  bnj553  34895  bnj964  34940  cusgredgex  35116  revwlk  35119  loop1cycl  35131  subfacp1lem3  35176  subfacp1lem5  35178  erdszelem9  35193  prv1n  35425  ply1divalg3  35636  quad3  35664  br6  35751  elintfv  35759  dfon2lem5  35782  dfon2lem8  35785  brbigcup  35893  dfbigcup2  35894  elfix  35898  ellimits  35905  snelsingles  35917  dfiota3  35918  imageval  35925  brapply  35933  brsuccf  35936  funpartlem  35937  brfullfun  35943  dfrecs2  35945  dfrdg4  35946  altopthbg  35963  altopthc  35966  altopthd  35967  altopelaltxp  35971  brsegle  36103  outsideofrflx  36122  elicc3  36312  nn0prpw  36318  opnregcld  36325  cldregopn  36326  fneval  36347  topfneec  36350  knoppndvlem9  36515  bj-elgab  36934  bj-gabima  36935  bj-elsngl  36963  bj-snglc  36964  bj-projval  36991  bj-disj2r  37023  bj-restreg  37094  bj-0int  37096  copsex2b  37135  bj-inftyexpitaudisj  37200  bj-inftyexpidisj  37205  bj-bary1lem1  37306  topdifinffinlem  37342  topdifinfeq  37345  fvineqsnf1  37405  curf  37599  uncf  37600  curunc  37603  unccur  37604  poimirlem2  37623  poimirlem16  37637  poimirlem17  37638  poimirlem19  37640  poimirlem20  37641  poimirlem27  37648  mblfinlem2  37659  mbfresfi  37667  itg2addnclem2  37673  ftc1anclem3  37696  fdc  37746  heibor1  37811  opidonOLD  37853  0rngo  38028  smprngopr  38053  isfldidl  38069  isfldidl2  38070  eqbrb  38228  eqelb  38230  ideq2  38302  relcnveq  38317  n0elqs  38321  disjressuc2  38381  elrelscnveq  38490  qseq  38647  disjdmqscossss  38802  lcvnbtwn3  39028  lcvexchlem1  39034  lsatnem0  39045  opcon1b  39198  omllaw2N  39244  cmtbr2N  39253  leatb  39292  cvlsupr2  39343  glbconxN  39379  islln3  39511  llnexatN  39522  islpln3  39534  lplnexatN  39564  islvol3  39577  dalem-cly  39672  isline4N  39778  2llnma3r  39789  poml4N  39954  4atex2  40078  4atex2-0bOLDN  40080  cdlemefrs29bpre0  40397  cdlemftr3  40566  cdlemb3  40607  cdlemg17h  40669  cdlemg17pq  40673  cdlemg19  40685  cdlemg21  40687  tendoex  40976  dva1dim  40986  dihglb2  41343  doch11  41374  dochsordN  41375  lcfrlem9  41551  hlhillcs  41959  lcmineqlem4  42027  aks6d1c7lem2  42176  aks5lem3a  42184  aks5lem6  42187  unitscyglem2  42191  unitscyglem3  42192  addsubeq4com  42275  ef11d  42334  fimgmcyclem  42528  fsuppind  42585  elrfirn  42690  isnacs2  42701  isnacs3  42705  fiphp3d  42814  wopprc  43026  islnm2  43074  kercvrlsm  43079  fgraphopab  43199  tfsconcatlem  43332  tfsconcatrn  43338  tfsconcat0i  43341  tfsconcat0b  43342  tfsconcatrev  43344  oaun3lem1  43370  oadif1lem  43375  oadif1  43376  rp-fakeuninass  43512  snen1g  43520  iscard4  43529  sqrtcval  43637  frege124d  43757  frege129d  43759  frege92  43951  dffrege99  43958  clsk3nimkb  44036  clsk1indlem4  44040  clsk1indlem1  44041  ntrclsiso  44063  ntrclsk3  44066  ntrclsk13  44067  ntrneik4w  44096  extoimad  44160  int-sqdefd  44177  int-sqgeq0d  44182  radcnvrat  44310  bcc0  44336  opelopab4  44548  eqsbc2VD  44836  fzisoeu  45305  iuneqfzuz  45338  supxrleubrnmptf  45454  rexanuz2nf  45495  fsummulc1f  45576  fsumiunss  45580  fmul01lt1lem2  45590  sumnnodd  45635  fnlimfvre2  45682  limsupreuz  45742  limsupvaluz2  45743  liminfvalxr  45788  icccncfext  45892  cncfiooicc  45899  cncfioobdlem  45901  dvmptmulf  45942  dvmptfprodlem  45949  volioc  45977  itgioocnicc  45982  fourierdlem12  46124  fourierdlem20  46132  fourierdlem25  46137  fourierdlem33  46145  fourierdlem42  46154  fourierdlem52  46163  fourierdlem54  46165  fourierdlem57  46168  fourierdlem58  46169  fourierdlem59  46170  fourierdlem63  46174  fourierdlem65  46176  fourierdlem68  46179  fourierdlem73  46184  fourierdlem74  46185  fourierdlem75  46186  fourierdlem80  46191  fourierdlem81  46192  rrndistlt  46295  sge0ltfirpmpt2  46431  sge0pnfmpt  46450  hoidmv1le  46599  hoidmvle  46605  vonioolem2  46686  smflimlem3  46778  lambert0  46895  lamberte  46896  euabsneu  47033  funressnfv  47048  aiotaval  47100  reuf1odnf  47112  reuf1od  47113  afvpcfv0  47151  dfafn5a  47165  afvelrnb  47168  afvelrnb0  47169  dfaimafn2  47171  dfatsnafv2  47257  dfatdmfcoafv2  47259  f1oresf1o2  47296  ceilbi  47338  minusmodnep2tmod  47358  0nelsetpreimafv  47395  fargshiftfo  47447  sprsymrelf1  47501  reupr  47527  fmtnorec2lem  47547  fmtnoprmfac1  47570  fmtnoprmfac2  47572  sfprmdvdsmersenne  47608  lighneallem2  47611  dfeven2  47654  dfodd3  47655  odd2np1ALTV  47679  even3prm2  47724  fppr2odd  47736  nnsum3primesgbe  47797  nnsum3primesle9  47799  clnbgrsym  47842  dfvopnbgr2  47857  isuspgrim0  47898  isuspgrimlem  47899  dfgric2  47919  grtriprop  47944  uspgrlimlem3  47993  gpgvtxedg1  48059  pgnbgreunbgrlem2lem1  48108  pgnbgreunbgrlem2lem2  48109  0nodd  48162  2nodd  48164  lmod0rng  48221  rngcinvALTV  48268  ringcinvALTV  48302  lcoel0  48421  lindslinindimp2lem4  48454  ldepspr  48466  lincresunit3  48474  nn0sumshdiglemB  48613  nn0sumshdiglem1  48614  rrx2pnedifcoorneorr  48710  eenglngeehlnmlem1  48730  eenglngeehlnmlem2  48731  rrx2linest  48735  rrx2linest2  48737  rrxsphere  48741  line2ylem  48744  line2x  48747  itscnhlc0xyqsol  48758  itschlc0xyqsol1  48759  itsclinecirc0b  48767  2itscp  48774  inlinecirc02plem  48779  brab2dd  48820  uptr2  49214