Theorem eqcom 2745

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

Syntax hints:   ↔ wb 205   = wceq 1539

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-cleq 2730

This theorem is referenced by:  eqcoms  2746  eqcomi  2747  neqcomd  2748  eqeq2d  2749  eqtr2OLD  2763  eqtr3OLD  2765  abeq1  2872  necom  2996  nesym  2999  pm13.181OLD  3026  gencbvex  3478  clel5  3589  eqsbc2  3781  dfss  3901  sspsstri  4033  ssnelpss  4042  ssdifim  4193  disj  4378  disj4  4389  reuprg0  4635  preq1b  4774  invdisj  5054  disjprgw  5065  disjprg  5066  dtruALT  5306  reusv3  5323  dtruALT2  5353  opthg2  5388  copsex2g  5401  copsex4g  5403  opcom  5409  opeqsng  5411  opeqpr  5413  snopeqop  5414  propeqop  5415  opthwiener  5422  vopelopabsb  5435  opthprc  5642  elxp3  5644  relop  5748  dmopab3  5817  rncoeq  5873  restidsing  5951  somin1  6027  xpcan  6068  xpcan2  6069  dfrel4v  6082  dmsnn0  6099  reu3op  6184  reuop  6185  opreu2reurex  6186  ordtri2  6286  ordtri2or3  6348  suc11  6354  on0eqel  6369  snsn0non  6370  iota1  6395  iotan0  6408  sniota  6409  mptfnf  6552  fresaunres1  6631  dffn5  6810  fvelrnb  6812  dfimafn2  6815  funimass4  6816  feqmptdf  6821  fnsnfv  6829  fnsnfvOLD  6830  dmfco  6846  fndmdif  6901  fneqeql  6905  rexrn  6945  ralrn  6946  elrnrexdmb  6948  dffo4  6961  funopsn  7002  ftpg  7010  fprb  7051  rexima  7095  ralima  7096  fvclss  7097  dff13  7109  f1eqcocnv  7153  f1eqcocnvOLD  7154  riotaeqimp  7239  eusvobj2  7248  f1ocnvfv3  7251  oprabidw  7286  oprabid  7287  oprabv  7313  eloprabga  7360  eloprabgaOLD  7361  ovelimab  7428  onmindif2  7634  br1steqg  7826  br2ndeqg  7827  dfoprab3  7867  opiota  7872  f1o2ndf1  7934  brtpos2  8019  tpossym  8045  mpocurryd  8056  rdglim2  8234  tz7.48lem  8242  oaf1o  8356  omopthi  8451  erth2  8506  brecop  8557  erovlem  8560  ecopovsym  8566  eceqoveq  8569  xpcomco  8802  omxpenlem  8813  mapen  8877  nneneq  8896  unxpdomlem3  8958  unfilem1  9008  mapfien  9097  supgtoreq  9159  wemapsolem  9239  suc11reg  9307  inf3lem2  9317  inf3lem6  9321  djulf1o  9601  djurf1o  9602  infenaleph  9778  isinfcard  9779  dfac5  9815  cfeq0  9943  cfsuc  9944  ssfin4  9997  fin23lem25  10011  fin23lem22  10014  fin23lem40  10038  fin1a2lem5  10091  axcclem  10144  brdom7disj  10218  brdom6disj  10219  inar1  10462  psslinpr  10718  ltexprlem4  10726  ltsrpr  10764  mulgt0sr  10792  elreal  10818  ltresr  10827  leloe  10992  eqlei2  11016  addsubeq4  11166  subcan2  11176  negcon1  11203  negcon2  11204  addid0  11324  addeq0  11328  divmul2  11567  conjmul  11622  rereccl  11623  creur  11897  creui  11898  nndiv  11949  nn0sub  12213  elnn0z  12262  elznn0  12264  xrleloe  12807  ngtmnft  12829  icoshftf1o  13135  iccf1o  13157  fzen  13202  fzneuz  13266  injresinj  13436  fleqceilz  13502  mod0  13524  modmuladdnn0  13563  modirr  13590  addmodlteq  13594  nn0ennn  13627  hashrabsn01  14016  hashsdom  14024  hashgt12el2  14066  hashbclem  14092  hashfacen  14094  hashfacenOLD  14095  hashf1lem1  14096  hashf1lem1OLD  14097  hashtpg  14127  fi1uzind  14139  ccatw2s1p1  14274  ccatw2s1p1OLD  14275  wrd2ind  14364  cshw1  14463  scshwfzeqfzo  14467  s2f1o  14557  wwlktovfo  14601  dmtrclfv  14657  cjreb  14762  leabs  14939  reusq0  15102  incexc2  15478  rpnnen2lem12  15862  dvdsval2  15894  dvdsabseq  15950  dvdsflip  15954  odd2np1  15978  oddm1even  15980  sqoddm1div8z  15991  m1exp1  16013  divalglem4  16033  divalglem8  16037  divalgb  16041  modremain  16045  zeqzmulgcd  16145  dfgcd2  16182  lcmfpr  16260  lcmftp  16269  lcmfunsnlem2  16273  divgcdcoprm0  16298  prm2orodd  16324  hashdvds  16404  oddprmdvds  16532  vdwlem12  16621  cshwshashlem1  16725  cshwsiun  16729  initoid  17632  termoid  17633  setcinv  17721  yonedainv  17915  joinfval  18006  joinfval2  18007  meetfval  18020  meetfval2  18021  latnle  18106  sgrp2nmndlem3  18479  grpid  18530  grpinvcnv  18558  grplmulf1o  18564  grpsubeq0  18576  grpsubadd  18578  grplactcnv  18593  isnsg4  18710  cycsubmel  18734  conjghm  18780  conjnmzb  18784  gacan  18826  gapm  18827  cntzrec  18855  oppgcntz  18886  fvcosymgeq  18952  odmulgeq  19079  dfod2  19086  sylow3lem3  19149  sylow3lem6  19152  lssnle  19195  lsmhash  19226  efgredlemb  19267  efgrelexlemb  19271  dprd2d2  19562  ablfac1eulem  19590  pgpfac1lem2  19593  pgpfac1lem4  19596  dvdsrval  19802  dvdsr02  19813  rmodislmodlem  20105  lvecinv  20290  rspsn  20438  0ring01eqbi  20457  prmirredlem  20606  zndvds  20669  znleval  20674  psrbagconf1o  21049  psrbagconf1oOLD  21050  mplmonmul  21147  gsummoncoe1  21385  mat1dimelbas  21528  mat1dimbas  21529  1mavmul  21605  ma1repveval  21628  mulmarep1gsum1  21630  mdetunilem9  21677  m2cpminvid2lem  21811  pmatcollpw3lem  21840  mp2pm2mplem4  21866  toponsspwpw  21979  dmtopon  21980  cmpfi  22467  ssref  22571  qtopeu  22775  hmeoimaf1o  22829  txhmeo  22862  fbasrn  22943  rnelfmlem  23011  hauspwpwf1  23046  alexsubALTlem4  23109  qustgpopn  23179  qustgphaus  23182  fmucndlem  23351  isngp3  23660  isngp4  23674  metnrmlem1a  23927  icopnfcnv  24011  iccpnfcnv  24013  ivthle  24525  ivthle2  24526  dyadmbl  24669  mbfinf  24734  i1fmulclem  24772  itg1mulc  24774  mvth  25061  dvivth  25079  lhop2  25084  dvdsq1p  25230  reeff1o  25511  coseq1  25586  recosf1o  25596  resinf1o  25597  efopn  25718  cxpeq  25815  logreclem  25817  affineequiv  25878  affineequiv4  25881  affineequivne  25882  quad2  25894  dcubic  25901  mcubic  25902  quart  25916  atandm2  25932  rlimcnp2  26021  amgm  26045  wilthlem2  26123  mumullem2  26234  sqff1o  26236  dvdsflf1o  26241  gausslemma2dlem0i  26417  lgseisenlem2  26429  lgsquadlem2  26434  2lgslem1c  26446  2lgsoddprmlem2  26462  2lgsoddprm  26469  2sq2  26486  addsq2reu  26493  2sqreultlem  26500  2sqreunnltlem  26503  2sqreulem3  26506  tgjustf  26738  legtrid  26856  legso  26864  islmib  27052  lmicom  27053  lmiinv  27057  lmimid  27059  lmiopp  27067  colinearalglem2  27178  colinearalg  27181  ax5seglem4  27203  ax5seglem5  27204  axlowdimlem13  27225  axeuclidlem  27233  axeuclid  27234  axcontlem2  27236  axcontlem4  27238  elntg2  27256  structiedg0val  27295  usgredgsscusgredg  27729  fusgrn0degnn0  27769  umgr2v2evtxel  27792  vdiscusgrb  27800  uspgr2wlkeq  27915  wlk0prc  27923  wlklenvclwlk  27924  wlklenvclwlkOLD  27925  wlkp1lem8  27950  spthdep  28003  usgr2pthlem  28032  usgr2pth  28033  wlkiswwlksupgr2  28143  wlklnwwlkln2lem  28148  wwlksnextproplem3  28177  umgr2adedgwlk  28211  umgr2adedgspth  28214  umgr2wlkon  28216  umgrwwlks2on  28223  elwwlks2  28232  elwspths2spth  28233  clwlkclwwlklem2a4  28262  clwlkclwwlklem2  28265  erclwwlkref  28285  clwwlkf  28312  erclwwlknref  28334  erclwwlknsym  28335  erclwwlkntr  28336  hashecclwwlkn1  28342  umgrhashecclwwlk  28343  eupth2lem2  28484  eucrct2eupth  28510  numclwwlkqhash  28640  isgrpo  28760  hvsubaddi  29329  hire  29357  shmodsi  29652  omlsilem  29665  chcon1i  29728  chnlei  29748  pjoml3i  29849  cmbr2i  29859  chscllem2  29901  adjsym  30096  eigorthi  30100  dfadj2  30148  adjval2  30154  cnvadj  30155  dmadjrnb  30169  adjvalval  30200  cnlnadjeui  30340  cnlnssadj  30343  adjbdln  30346  pjimai  30439  pjin2i  30456  pjin3i  30457  stadd3i  30511  largei  30530  cvnbtwn3  30551  cvnbtwn4  30552  mddmd2  30572  superpos  30617  atnemeq0  30640  sumdmdii  30678  sumdmdlem  30681  addltmulALT  30709  opreu2reuALT  30726  foresf1o  30751  difeq  30766  disjrdx  30831  fcoinvbr  30848  fmptco1f1o  30869  dfimafnf  30872  funcnvmpt  30906  curry2ima  30943  intimafv  30945  cnvoprabOLD  30957  elicoelioo  31001  wrdt2ind  31127  swrdrn3  31129  orngsqr  31405  qusker  31451  eqg0el  31459  lsmsnorb  31481  zarcls  31726  xrmulc1cn  31782  xrge0iifcnv  31785  ind1a  31887  esumfsup  31938  esumpcvgval  31946  esumcvg  31954  esum2dlem  31960  issgon  31991  eulerpartgbij  32239  eulerpartlemgh  32245  ballotlemsima  32382  bnj1366  32709  bnj553  32778  bnj964  32823  cusgredgex  32983  revwlk  32986  loop1cycl  32999  subfacp1lem3  33044  subfacp1lem5  33046  erdszelem9  33061  prv1n  33293  quad3  33528  fnssintima  33578  imaeqsexv  33593  br6  33630  elintfv  33644  dfon2lem5  33669  dfon2lem8  33672  ttrcltr  33702  soseq  33730  sltval2  33786  sltintdifex  33791  sltres  33792  nosepon  33795  noextenddif  33798  nosepssdm  33816  nogt01o  33826  nosupprefixmo  33830  noinfprefixmo  33831  nosupno  33833  noinfno  33848  sleloe  33884  eqscut2  33927  scutbdaylt  33939  elold  33980  made0  33984  lrrecfr  34027  brbigcup  34127  dfbigcup2  34128  elfix  34132  ellimits  34139  snelsingles  34151  dfiota3  34152  imageval  34159  brapply  34167  brsuccf  34170  funpartlem  34171  brfullfun  34177  dfrecs2  34179  dfrdg4  34180  altopthbg  34197  altopthc  34200  altopthd  34201  altopelaltxp  34205  brsegle  34337  outsideofrflx  34356  elicc3  34433  nn0prpw  34439  opnregcld  34446  cldregopn  34447  fneval  34468  topfneec  34471  knoppndvlem9  34627  bj-elgab  35054  bj-gabima  35055  bj-elsngl  35085  bj-snglc  35086  bj-projval  35113  bj-disj2r  35145  bj-restreg  35197  bj-0int  35199  copsex2b  35238  bj-inftyexpitaudisj  35303  bj-inftyexpidisj  35308  bj-bary1lem1  35409  topdifinffinlem  35445  topdifinfeq  35448  fvineqsnf1  35508  curf  35682  uncf  35683  curunc  35686  unccur  35687  poimirlem2  35706  poimirlem16  35720  poimirlem17  35721  poimirlem19  35723  poimirlem20  35724  poimirlem27  35731  mblfinlem2  35742  mbfresfi  35750  itg2addnclem2  35756  ftc1anclem3  35779  fdc  35830  heibor1  35895  opidonOLD  35937  0rngo  36112  smprngopr  36137  isfldidl  36153  isfldidl2  36154  eqelb  36309  ideq2  36370  relcnveq  36384  n0elqs  36388  elrelscnveq  36537  lcvnbtwn3  36969  lcvexchlem1  36975  lsatnem0  36986  opcon1b  37139  omllaw2N  37185  cmtbr2N  37194  leatb  37233  cvlsupr2  37284  glbconxN  37319  islln3  37451  llnexatN  37462  islpln3  37474  lplnexatN  37504  islvol3  37517  dalem-cly  37612  isline4N  37718  2llnma3r  37729  poml4N  37894  4atex2  38018  4atex2-0bOLDN  38020  cdlemefrs29bpre0  38337  cdlemftr3  38506  cdlemb3  38547  cdlemg17h  38609  cdlemg17pq  38613  cdlemg19  38625  cdlemg21  38627  tendoex  38916  dva1dim  38926  dihglb2  39283  doch11  39314  dochsordN  39315  lcfrlem9  39491  hlhillcs  39903  lcmineqlem4  39968  metakunt1  40053  metakunt6  40058  metakunt15  40067  metakunt16  40068  fsuppind  40202  addsubeq4com  40229  elrfirn  40433  isnacs2  40444  isnacs3  40448  fiphp3d  40557  wopprc  40768  islnm2  40819  kercvrlsm  40824  fgraphopab  40951  rp-fakeuninass  41021  snen1g  41029  iscard4  41038  sqrtcval  41138  frege124d  41258  frege129d  41260  frege92  41452  dffrege99  41459  clsk3nimkb  41539  clsk1indlem4  41543  clsk1indlem1  41544  ntrclsiso  41566  ntrclsk3  41569  ntrclsk13  41570  ntrneik4w  41599  extoimad  41664  int-sqdefd  41681  int-sqgeq0d  41686  radcnvrat  41821  bcc0  41847  opelopab4  42060  eqsbc2VD  42349  fzisoeu  42729  iuneqfzuz  42764  supxrleubrnmptf  42881  fsummulc1f  43002  fsumiunss  43006  fmul01lt1lem2  43016  sumnnodd  43061  fnlimfvre2  43108  limsupreuz  43168  limsupvaluz2  43169  liminfvalxr  43214  icccncfext  43318  cncfiooicc  43325  cncfioobdlem  43327  dvmptmulf  43368  dvmptfprodlem  43375  volioc  43403  itgioocnicc  43408  fourierdlem12  43550  fourierdlem20  43558  fourierdlem25  43563  fourierdlem33  43571  fourierdlem42  43580  fourierdlem52  43589  fourierdlem54  43591  fourierdlem57  43594  fourierdlem58  43595  fourierdlem59  43596  fourierdlem63  43600  fourierdlem65  43602  fourierdlem68  43605  fourierdlem73  43610  fourierdlem74  43611  fourierdlem75  43612  fourierdlem80  43617  fourierdlem81  43618  rrndistlt  43721  sge0ltfirpmpt2  43854  sge0pnfmpt  43873  hoidmv1le  44022  hoidmvle  44028  vonioolem2  44109  smflimlem3  44195  euabsneu  44409  funressnfv  44424  aiotaval  44474  reuf1odnf  44486  reuf1od  44487  afvpcfv0  44525  dfafn5a  44539  afvelrnb  44542  afvelrnb0  44543  dfaimafn2  44545  dfatsnafv2  44631  dfatdmfcoafv2  44633  f1oresf1o2  44670  0nelsetpreimafv  44730  fargshiftfo  44782  sprsymrelf1  44836  reupr  44862  fmtnorec2lem  44882  fmtnoprmfac1  44905  fmtnoprmfac2  44907  sfprmdvdsmersenne  44943  lighneallem2  44946  dfeven2  44989  dfodd3  44990  odd2np1ALTV  45014  even3prm2  45059  fppr2odd  45071  nnsum3primesgbe  45132  nnsum3primesle9  45134  isomuspgrlem2d  45171  0nodd  45252  2nodd  45254  lmod0rng  45314  rngcinv  45427  rngcinvALTV  45439  ringcinv  45478  ringcinvALTV  45502  lcoel0  45657  lindslinindimp2lem4  45690  ldepspr  45702  lincresunit3  45710  nn0sumshdiglemB  45854  nn0sumshdiglem1  45855  rrx2pnedifcoorneorr  45951  eenglngeehlnmlem1  45971  eenglngeehlnmlem2  45972  rrx2linest  45976  rrx2linest2  45978  rrxsphere  45982  line2ylem  45985  line2x  45988  itscnhlc0xyqsol  45999  itschlc0xyqsol1  46000  itsclinecirc0b  46008  2itscp  46015  inlinecirc02plem  46020