Theorem eqcom 2746

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 2745	. 2 ⊢ (𝐴 = 𝐵 → 𝐵 = 𝐴)
3		id 22	. . 3 ⊢ (𝐵 = 𝐴 → 𝐵 = 𝐴)
4	3	eqcomd 2745	. 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 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-cleq 2731

This theorem is referenced by:  eqcoms  2747  eqcomi  2748  neqcomd  2749  eqeq2d  2750  eqtr2OLD  2764  eqtr3OLD  2766  abeq1  2874  necom  2998  nesym  3001  pm13.181OLD  3028  gencbvex  3489  clel5  3597  eqsbc2  3786  dfss  3906  sspsstri  4038  ssnelpss  4047  ssdifim  4197  disj  4382  disj4  4393  reuprg0  4639  preq1b  4778  invdisj  5059  disjprgw  5070  disjprg  5071  dtruALT  5312  reusv3  5329  opthg2  5395  copsex2g  5408  copsex4g  5410  opcom  5416  opeqsng  5418  opeqpr  5420  snopeqop  5421  propeqop  5422  opthwiener  5429  vopelopabsb  5443  opthprc  5652  elxp3  5654  relop  5762  dmopab3  5831  rncoeq  5887  restidsing  5965  somin1  6043  xpcan  6084  xpcan2  6085  dfrel4v  6098  dmsnn0  6115  reu3op  6199  reuop  6200  opreu2reurex  6201  ordtri2  6305  ordtri2or3  6367  suc11  6373  on0eqel  6388  snsn0non  6389  iota1  6414  iotan0  6427  sniota  6428  mptfnf  6577  fresaunres1  6656  dffn5  6837  fvelrnb  6839  dfimafn2  6842  funimass4  6843  feqmptdf  6848  fnsnfv  6856  fnsnfvOLD  6857  dmfco  6873  fndmdif  6928  fneqeql  6932  rexrn  6972  ralrn  6973  elrnrexdmb  6975  dffo4  6988  funopsn  7029  ftpg  7037  fprb  7078  rexima  7122  ralima  7123  fvclss  7124  dff13  7137  f1eqcocnv  7182  f1eqcocnvOLD  7183  riotaeqimp  7268  eusvobj2  7277  f1ocnvfv3  7280  oprabidw  7315  oprabid  7316  oprabv  7344  eloprabga  7391  eloprabgaOLD  7392  ovelimab  7459  onmindif2  7666  br1steqg  7862  br2ndeqg  7863  dfoprab3  7903  opiota  7908  f1o2ndf1  7972  brtpos2  8057  tpossym  8083  mpocurryd  8094  rdglim2  8272  tz7.48lem  8281  oaf1o  8403  omopthi  8500  erth2  8557  brecop  8608  erovlem  8611  ecopovsym  8617  eceqoveq  8620  xpcomco  8858  omxpenlem  8869  mapen  8937  nneneq  9001  nneneqOLD  9013  unxpdomlem3  9038  unfilem1  9087  mapfien  9176  supgtoreq  9238  wemapsolem  9318  suc11reg  9386  inf3lem2  9396  inf3lem6  9400  ttrcltr  9483  djulf1o  9679  djurf1o  9680  infenaleph  9856  isinfcard  9857  dfac5  9893  cfeq0  10021  cfsuc  10022  ssfin4  10075  fin23lem25  10089  fin23lem22  10092  fin23lem40  10116  fin1a2lem5  10169  axcclem  10222  brdom7disj  10296  brdom6disj  10297  inar1  10540  psslinpr  10796  ltexprlem4  10804  ltsrpr  10842  mulgt0sr  10870  elreal  10896  ltresr  10905  leloe  11070  eqlei2  11095  addsubeq4  11245  subcan2  11255  negcon1  11282  negcon2  11283  addid0  11403  addeq0  11407  divmul2  11646  conjmul  11701  rereccl  11702  creur  11976  creui  11977  nndiv  12028  nn0sub  12292  elnn0z  12341  elznn0  12343  xrleloe  12887  ngtmnft  12909  icoshftf1o  13215  iccf1o  13237  fzen  13282  fzneuz  13346  injresinj  13517  fleqceilz  13583  mod0  13605  modmuladdnn0  13644  modirr  13671  addmodlteq  13675  nn0ennn  13708  hashrabsn01  14097  hashsdom  14105  hashgt12el2  14147  hashbclem  14173  hashfacen  14175  hashfacenOLD  14176  hashf1lem1  14177  hashf1lem1OLD  14178  hashtpg  14208  fi1uzind  14220  ccatw2s1p1  14355  ccatw2s1p1OLD  14356  wrd2ind  14445  cshw1  14544  scshwfzeqfzo  14548  s2f1o  14638  wwlktovfo  14682  dmtrclfv  14738  cjreb  14843  leabs  15020  reusq0  15183  incexc2  15559  rpnnen2lem12  15943  dvdsval2  15975  dvdsabseq  16031  dvdsflip  16035  odd2np1  16059  oddm1even  16061  sqoddm1div8z  16072  m1exp1  16094  divalglem4  16114  divalglem8  16118  divalgb  16122  modremain  16126  zeqzmulgcd  16226  dfgcd2  16263  lcmfpr  16341  lcmftp  16350  lcmfunsnlem2  16354  divgcdcoprm0  16379  prm2orodd  16405  hashdvds  16485  oddprmdvds  16613  vdwlem12  16702  cshwshashlem1  16806  cshwsiun  16810  initoid  17725  termoid  17726  setcinv  17814  yonedainv  18008  joinfval  18100  joinfval2  18101  meetfval  18114  meetfval2  18115  latnle  18200  sgrp2nmndlem3  18573  grpid  18624  grpinvcnv  18652  grplmulf1o  18658  grpsubeq0  18670  grpsubadd  18672  grplactcnv  18687  isnsg4  18804  cycsubmel  18828  conjghm  18874  conjnmzb  18878  gacan  18920  gapm  18921  cntzrec  18949  oppgcntz  18980  fvcosymgeq  19046  odmulgeq  19173  dfod2  19180  sylow3lem3  19243  sylow3lem6  19246  lssnle  19289  lsmhash  19320  efgredlemb  19361  efgrelexlemb  19365  dprd2d2  19656  ablfac1eulem  19684  pgpfac1lem2  19687  pgpfac1lem4  19690  dvdsrval  19896  dvdsr02  19907  rmodislmodlem  20199  lvecinv  20384  rspsn  20534  0ring01eqbi  20553  prmirredlem  20703  zndvds  20766  znleval  20771  psrbagconf1o  21148  psrbagconf1oOLD  21149  mplmonmul  21246  gsummoncoe1  21484  mat1dimelbas  21629  mat1dimbas  21630  1mavmul  21706  ma1repveval  21729  mulmarep1gsum1  21731  mdetunilem9  21778  m2cpminvid2lem  21912  pmatcollpw3lem  21941  mp2pm2mplem4  21967  toponsspwpw  22080  dmtopon  22081  cmpfi  22568  ssref  22672  qtopeu  22876  hmeoimaf1o  22930  txhmeo  22963  fbasrn  23044  rnelfmlem  23112  hauspwpwf1  23147  alexsubALTlem4  23210  qustgpopn  23280  qustgphaus  23283  fmucndlem  23452  isngp3  23763  isngp4  23777  metnrmlem1a  24030  icopnfcnv  24114  iccpnfcnv  24116  ivthle  24629  ivthle2  24630  dyadmbl  24773  mbfinf  24838  i1fmulclem  24876  itg1mulc  24878  mvth  25165  dvivth  25183  lhop2  25188  dvdsq1p  25334  reeff1o  25615  coseq1  25690  recosf1o  25700  resinf1o  25701  efopn  25822  cxpeq  25919  logreclem  25921  affineequiv  25982  affineequiv4  25985  affineequivne  25986  quad2  25998  dcubic  26005  mcubic  26006  quart  26020  atandm2  26036  rlimcnp2  26125  amgm  26149  wilthlem2  26227  mumullem2  26338  sqff1o  26340  dvdsflf1o  26345  gausslemma2dlem0i  26521  lgseisenlem2  26533  lgsquadlem2  26538  2lgslem1c  26550  2lgsoddprmlem2  26566  2lgsoddprm  26573  2sq2  26590  addsq2reu  26597  2sqreultlem  26604  2sqreunnltlem  26607  2sqreulem3  26610  tgjustf  26843  legtrid  26961  legso  26969  islmib  27157  lmicom  27158  lmiinv  27162  lmimid  27164  lmiopp  27172  colinearalglem2  27284  colinearalg  27287  ax5seglem4  27309  ax5seglem5  27310  axlowdimlem13  27331  axeuclidlem  27339  axeuclid  27340  axcontlem2  27342  axcontlem4  27344  elntg2  27362  structiedg0val  27401  usgredgsscusgredg  27835  fusgrn0degnn0  27875  umgr2v2evtxel  27898  vdiscusgrb  27906  uspgr2wlkeq  28022  wlk0prc  28030  wlklenvclwlk  28031  wlklenvclwlkOLD  28032  wlkp1lem8  28057  spthdep  28111  usgr2pthlem  28140  usgr2pth  28141  wlkiswwlksupgr2  28251  wlklnwwlkln2lem  28256  wwlksnextproplem3  28285  umgr2adedgwlk  28319  umgr2adedgspth  28322  umgr2wlkon  28324  umgrwwlks2on  28331  elwwlks2  28340  elwspths2spth  28341  clwlkclwwlklem2a4  28370  clwlkclwwlklem2  28373  erclwwlkref  28393  clwwlkf  28420  erclwwlknref  28442  erclwwlknsym  28443  erclwwlkntr  28444  hashecclwwlkn1  28450  umgrhashecclwwlk  28451  eupth2lem2  28592  eucrct2eupth  28618  numclwwlkqhash  28748  isgrpo  28868  hvsubaddi  29437  hire  29465  shmodsi  29760  omlsilem  29773  chcon1i  29836  chnlei  29856  pjoml3i  29957  cmbr2i  29967  chscllem2  30009  adjsym  30204  eigorthi  30208  dfadj2  30256  adjval2  30262  cnvadj  30263  dmadjrnb  30277  adjvalval  30308  cnlnadjeui  30448  cnlnssadj  30451  adjbdln  30454  pjimai  30547  pjin2i  30564  pjin3i  30565  stadd3i  30619  largei  30638  cvnbtwn3  30659  cvnbtwn4  30660  mddmd2  30680  superpos  30725  atnemeq0  30748  sumdmdii  30786  sumdmdlem  30789  addltmulALT  30817  opreu2reuALT  30834  foresf1o  30859  difeq  30874  disjrdx  30939  fcoinvbr  30956  fmptco1f1o  30977  dfimafnf  30980  funcnvmpt  31013  curry2ima  31050  intimafv  31052  cnvoprabOLD  31064  elicoelioo  31108  wrdt2ind  31234  swrdrn3  31236  orngsqr  31512  qusker  31558  eqg0el  31566  lsmsnorb  31588  zarcls  31833  xrmulc1cn  31889  xrge0iifcnv  31892  ind1a  31996  esumfsup  32047  esumpcvgval  32055  esumcvg  32063  esum2dlem  32069  issgon  32100  eulerpartgbij  32348  eulerpartlemgh  32354  ballotlemsima  32491  bnj1366  32818  bnj553  32887  bnj964  32932  cusgredgex  33092  revwlk  33095  loop1cycl  33108  subfacp1lem3  33153  subfacp1lem5  33155  erdszelem9  33170  prv1n  33402  quad3  33637  fnssintima  33685  imaeqsexv  33699  br6  33733  elintfv  33747  dfon2lem5  33772  dfon2lem8  33775  soseq  33812  sltval2  33868  sltintdifex  33873  sltres  33874  nosepon  33877  noextenddif  33880  nosepssdm  33898  nogt01o  33908  nosupprefixmo  33912  noinfprefixmo  33913  nosupno  33915  noinfno  33930  sleloe  33966  eqscut2  34009  scutbdaylt  34021  elold  34062  made0  34066  lrrecfr  34109  brbigcup  34209  dfbigcup2  34210  elfix  34214  ellimits  34221  snelsingles  34233  dfiota3  34234  imageval  34241  brapply  34249  brsuccf  34252  funpartlem  34253  brfullfun  34259  dfrecs2  34261  dfrdg4  34262  altopthbg  34279  altopthc  34282  altopthd  34283  altopelaltxp  34287  brsegle  34419  outsideofrflx  34438  elicc3  34515  nn0prpw  34521  opnregcld  34528  cldregopn  34529  fneval  34550  topfneec  34553  knoppndvlem9  34709  bj-elgab  35136  bj-gabima  35137  bj-elsngl  35167  bj-snglc  35168  bj-projval  35195  bj-disj2r  35227  bj-restreg  35279  bj-0int  35281  copsex2b  35320  bj-inftyexpitaudisj  35385  bj-inftyexpidisj  35390  bj-bary1lem1  35491  topdifinffinlem  35527  topdifinfeq  35530  fvineqsnf1  35590  curf  35764  uncf  35765  curunc  35768  unccur  35769  poimirlem2  35788  poimirlem16  35802  poimirlem17  35803  poimirlem19  35805  poimirlem20  35806  poimirlem27  35813  mblfinlem2  35824  mbfresfi  35832  itg2addnclem2  35838  ftc1anclem3  35861  fdc  35912  heibor1  35977  opidonOLD  36019  0rngo  36194  smprngopr  36219  isfldidl  36235  isfldidl2  36236  eqelb  36391  ideq2  36450  relcnveq  36464  n0elqs  36468  elrelscnveq  36617  lcvnbtwn3  37049  lcvexchlem1  37055  lsatnem0  37066  opcon1b  37219  omllaw2N  37265  cmtbr2N  37274  leatb  37313  cvlsupr2  37364  glbconxN  37399  islln3  37531  llnexatN  37542  islpln3  37554  lplnexatN  37584  islvol3  37597  dalem-cly  37692  isline4N  37798  2llnma3r  37809  poml4N  37974  4atex2  38098  4atex2-0bOLDN  38100  cdlemefrs29bpre0  38417  cdlemftr3  38586  cdlemb3  38627  cdlemg17h  38689  cdlemg17pq  38693  cdlemg19  38705  cdlemg21  38707  tendoex  38996  dva1dim  39006  dihglb2  39363  doch11  39394  dochsordN  39395  lcfrlem9  39571  hlhillcs  39983  lcmineqlem4  40047  metakunt1  40132  metakunt6  40137  metakunt15  40146  metakunt16  40147  fsuppind  40286  addsubeq4com  40315  elrfirn  40524  isnacs2  40535  isnacs3  40539  fiphp3d  40648  wopprc  40859  islnm2  40910  kercvrlsm  40915  fgraphopab  41042  rp-fakeuninass  41130  snen1g  41138  iscard4  41147  sqrtcval  41256  frege124d  41376  frege129d  41378  frege92  41570  dffrege99  41577  clsk3nimkb  41657  clsk1indlem4  41661  clsk1indlem1  41662  ntrclsiso  41684  ntrclsk3  41687  ntrclsk13  41688  ntrneik4w  41717  extoimad  41782  int-sqdefd  41799  int-sqgeq0d  41804  radcnvrat  41939  bcc0  41965  opelopab4  42178  eqsbc2VD  42467  fzisoeu  42846  iuneqfzuz  42881  supxrleubrnmptf  42998  fsummulc1f  43119  fsumiunss  43123  fmul01lt1lem2  43133  sumnnodd  43178  fnlimfvre2  43225  limsupreuz  43285  limsupvaluz2  43286  liminfvalxr  43331  icccncfext  43435  cncfiooicc  43442  cncfioobdlem  43444  dvmptmulf  43485  dvmptfprodlem  43492  volioc  43520  itgioocnicc  43525  fourierdlem12  43667  fourierdlem20  43675  fourierdlem25  43680  fourierdlem33  43688  fourierdlem42  43697  fourierdlem52  43706  fourierdlem54  43708  fourierdlem57  43711  fourierdlem58  43712  fourierdlem59  43713  fourierdlem63  43717  fourierdlem65  43719  fourierdlem68  43722  fourierdlem73  43727  fourierdlem74  43728  fourierdlem75  43729  fourierdlem80  43734  fourierdlem81  43735  rrndistlt  43838  sge0ltfirpmpt2  43971  sge0pnfmpt  43990  hoidmv1le  44139  hoidmvle  44145  vonioolem2  44226  smflimlem3  44318  euabsneu  44533  funressnfv  44548  aiotaval  44598  reuf1odnf  44610  reuf1od  44611  afvpcfv0  44649  dfafn5a  44663  afvelrnb  44666  afvelrnb0  44667  dfaimafn2  44669  dfatsnafv2  44755  dfatdmfcoafv2  44757  f1oresf1o2  44794  0nelsetpreimafv  44853  fargshiftfo  44905  sprsymrelf1  44959  reupr  44985  fmtnorec2lem  45005  fmtnoprmfac1  45028  fmtnoprmfac2  45030  sfprmdvdsmersenne  45066  lighneallem2  45069  dfeven2  45112  dfodd3  45113  odd2np1ALTV  45137  even3prm2  45182  fppr2odd  45194  nnsum3primesgbe  45255  nnsum3primesle9  45257  isomuspgrlem2d  45294  0nodd  45375  2nodd  45377  lmod0rng  45437  rngcinv  45550  rngcinvALTV  45562  ringcinv  45601  ringcinvALTV  45625  lcoel0  45780  lindslinindimp2lem4  45813  ldepspr  45825  lincresunit3  45833  nn0sumshdiglemB  45977  nn0sumshdiglem1  45978  rrx2pnedifcoorneorr  46074  eenglngeehlnmlem1  46094  eenglngeehlnmlem2  46095  rrx2linest  46099  rrx2linest2  46101  rrxsphere  46105  line2ylem  46108  line2x  46111  itscnhlc0xyqsol  46122  itschlc0xyqsol1  46123  itsclinecirc0b  46131  2itscp  46138  inlinecirc02plem  46143