Theorem eqcom 2738

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

Syntax hints:   ↔ wb 205   = wceq 1541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-cleq 2723

This theorem is referenced by:  eqcoms  2739  eqcomi  2740  neqcomd  2741  eqeq2d  2742  eqtr2OLD  2756  eqtr3OLD  2758  eqabcb  2874  necom  2993  nesym  2996  pm13.181OLD  3023  gencbvex  3505  clel5  3620  eqsbc2  3811  dfss  3931  sspsstri  4067  ssnelpss  4076  ssdifim  4227  disj  4412  disj4  4423  reuprg0  4668  preq1b  4809  invdisj  5094  disjprgw  5105  disjprg  5106  dtruALT  5348  reusv3  5365  opthg2  5441  copsex2g  5455  copsex4g  5457  opcom  5463  opeqsng  5465  opeqpr  5467  snopeqop  5468  propeqop  5469  opthwiener  5476  vopelopabsb  5491  opthprc  5701  elxp3  5703  relop  5811  dmopab3  5880  rncoeq  5935  restidsing  6011  somin1  6092  xpcan  6133  xpcan2  6134  dfrel4v  6147  dmsnn0  6164  reu3op  6249  reuop  6250  opreu2reurex  6251  ordtri2  6357  ordtri2or3  6422  suc11  6429  on0eqel  6446  snsn0non  6447  iota1  6478  iotan0  6491  sniota  6492  mptfnf  6641  fresaunres1  6720  dffn5  6906  fvelrnb  6908  dfimafn2  6911  funimass4  6912  feqmptdf  6917  fnsnfv  6925  fnsnfvOLD  6926  dmfco  6942  fndmdif  6997  fneqeql  7001  rexrn  7042  ralrn  7043  elrnrexdmb  7045  dffo4  7058  funopsn  7099  ftpg  7107  fprb  7148  rexima  7192  ralima  7193  fvclss  7194  dff13  7207  f1eqcocnv  7252  f1eqcocnvOLD  7253  fnssintima  7312  imaeqsexv  7313  riotaeqimp  7345  eusvobj2  7354  f1ocnvfv3  7357  oprabidw  7393  oprabid  7394  oprabv  7422  eloprabga  7469  eloprabgaOLD  7470  ovelimab  7537  onmindif2  7747  br1steqg  7948  br2ndeqg  7949  dfoprab3  7991  opiota  7996  f1o2ndf1  8059  soseq  8096  brtpos2  8168  tpossym  8194  mpocurryd  8205  rdglim2  8383  tz7.48lem  8392  oaf1o  8515  omopthi  8612  erth2  8705  brecop  8756  erovlem  8759  ecopovsym  8765  eceqoveq  8768  xpcomco  9013  omxpenlem  9024  mapen  9092  nneneq  9160  nneneqOLD  9172  unxpdomlem3  9203  unfilem1  9261  mapfien  9353  supgtoreq  9415  wemapsolem  9495  suc11reg  9564  inf3lem2  9574  inf3lem6  9578  ttrcltr  9661  djulf1o  9857  djurf1o  9858  infenaleph  10036  isinfcard  10037  dfac5  10073  cfeq0  10201  cfsuc  10202  ssfin4  10255  fin23lem25  10269  fin23lem22  10272  fin23lem40  10296  fin1a2lem5  10349  axcclem  10402  brdom7disj  10476  brdom6disj  10477  inar1  10720  psslinpr  10976  ltexprlem4  10984  ltsrpr  11022  mulgt0sr  11050  elreal  11076  ltresr  11085  leloe  11250  eqlei2  11275  addsubeq4  11425  subcan2  11435  negcon1  11462  negcon2  11463  addid0  11583  addeq0  11587  divmul2  11826  conjmul  11881  rereccl  11882  creur  12156  creui  12157  nndiv  12208  nn0sub  12472  elnn0z  12521  elznn0  12523  xrleloe  13073  ngtmnft  13095  icoshftf1o  13401  iccf1o  13423  fzen  13468  fzneuz  13532  injresinj  13703  fleqceilz  13769  mod0  13791  modmuladdnn0  13830  modirr  13857  addmodlteq  13861  nn0ennn  13894  hashrabsn01  14283  hashsdom  14291  hashgt12el2  14333  hashbclem  14361  hashfacen  14363  hashfacenOLD  14364  hashf1lem1  14365  hashf1lem1OLD  14366  hashtpg  14396  fi1uzind  14408  ccatw2s1p1  14536  wrd2ind  14623  cshw1  14722  cshwsexa  14724  scshwfzeqfzo  14727  s2f1o  14817  wwlktovfo  14859  dmtrclfv  14915  cjreb  15020  leabs  15196  reusq0  15359  incexc2  15734  rpnnen2lem12  16118  dvdsval2  16150  dvdsabseq  16206  dvdsflip  16210  odd2np1  16234  oddm1even  16236  sqoddm1div8z  16247  m1exp1  16269  divalglem4  16289  divalglem8  16293  divalgb  16297  modremain  16301  zeqzmulgcd  16401  dfgcd2  16438  lcmfpr  16514  lcmftp  16523  lcmfunsnlem2  16527  divgcdcoprm0  16552  prm2orodd  16578  hashdvds  16658  oddprmdvds  16786  vdwlem12  16875  cshwshashlem1  16979  cshwsiun  16983  initoid  17901  termoid  17902  setcinv  17990  yonedainv  18184  joinfval  18276  joinfval2  18277  meetfval  18290  meetfval2  18291  latnle  18376  sgrp2nmndlem3  18749  grpid  18800  grpinvcnv  18829  grplmulf1o  18835  grpsubeq0  18847  grpsubadd  18849  grplactcnv  18864  isnsg4  18983  cycsubmel  19007  conjghm  19053  conjnmzb  19057  gacan  19099  gapm  19100  cntzrec  19128  oppgcntz  19159  fvcosymgeq  19225  odmulgeq  19353  dfod2  19360  sylow3lem3  19425  sylow3lem6  19428  lssnle  19470  lsmhash  19501  efgredlemb  19542  efgrelexlemb  19546  dprd2d2  19837  ablfac1eulem  19865  pgpfac1lem2  19868  pgpfac1lem4  19871  dvdsrval  20088  dvdsr02  20099  01eq0ring  20215  0ring01eqbi  20217  rmodislmodlem  20446  lvecinv  20633  rspsn  20783  prmirredlem  20930  zndvds  20993  znleval  20998  psrbagconf1o  21375  psrbagconf1oOLD  21376  mplmonmul  21474  gsummoncoe1  21712  mat1dimelbas  21857  mat1dimbas  21858  1mavmul  21934  ma1repveval  21957  mulmarep1gsum1  21959  mdetunilem9  22006  m2cpminvid2lem  22140  pmatcollpw3lem  22169  mp2pm2mplem4  22195  toponsspwpw  22308  dmtopon  22309  cmpfi  22796  ssref  22900  qtopeu  23104  hmeoimaf1o  23158  txhmeo  23191  fbasrn  23272  rnelfmlem  23340  hauspwpwf1  23375  alexsubALTlem4  23438  qustgpopn  23508  qustgphaus  23511  fmucndlem  23680  isngp3  23991  isngp4  24005  metnrmlem1a  24258  icopnfcnv  24342  iccpnfcnv  24344  ivthle  24857  ivthle2  24858  dyadmbl  25001  mbfinf  25066  i1fmulclem  25104  itg1mulc  25106  mvth  25393  dvivth  25411  lhop2  25416  dvdsq1p  25562  reeff1o  25843  coseq1  25918  recosf1o  25928  resinf1o  25929  efopn  26050  cxpeq  26147  logreclem  26149  affineequiv  26210  affineequiv4  26213  affineequivne  26214  quad2  26226  dcubic  26233  mcubic  26234  quart  26248  atandm2  26264  rlimcnp2  26353  amgm  26377  wilthlem2  26455  mumullem2  26566  sqff1o  26568  dvdsflf1o  26573  gausslemma2dlem0i  26749  lgseisenlem2  26761  lgsquadlem2  26766  2lgslem1c  26778  2lgsoddprmlem2  26794  2lgsoddprm  26801  2sq2  26818  addsq2reu  26825  2sqreultlem  26832  2sqreunnltlem  26835  2sqreulem3  26838  sltval2  27041  sltintdifex  27046  sltres  27047  nosepon  27050  noextenddif  27053  nosepssdm  27071  nogt01o  27081  nosupprefixmo  27085  noinfprefixmo  27086  nosupno  27088  noinfno  27103  sleloe  27139  eqscut2  27188  scutbdaylt  27200  elold  27242  made0  27246  lrrecfr  27298  subadds  27400  tgjustf  27478  legtrid  27596  legso  27604  islmib  27792  lmicom  27793  lmiinv  27797  lmimid  27799  lmiopp  27807  colinearalglem2  27919  colinearalg  27922  ax5seglem4  27944  ax5seglem5  27945  axlowdimlem13  27966  axeuclidlem  27974  axeuclid  27975  axcontlem2  27977  axcontlem4  27979  elntg2  27997  structiedg0val  28036  usgredgsscusgredg  28470  fusgrn0degnn0  28510  umgr2v2evtxel  28533  vdiscusgrb  28541  uspgr2wlkeq  28657  wlk0prc  28665  wlklenvclwlk  28666  wlkp1lem8  28691  spthdep  28745  usgr2pthlem  28774  usgr2pth  28775  wlkiswwlksupgr2  28885  wlklnwwlkln2lem  28890  wwlksnextproplem3  28919  umgr2adedgwlk  28953  umgr2adedgspth  28956  umgr2wlkon  28958  umgrwwlks2on  28965  elwwlks2  28974  elwspths2spth  28975  clwlkclwwlklem2a4  29004  clwlkclwwlklem2  29007  erclwwlkref  29027  clwwlkf  29054  erclwwlknref  29076  erclwwlknsym  29077  erclwwlkntr  29078  hashecclwwlkn1  29084  umgrhashecclwwlk  29085  eupth2lem2  29226  eucrct2eupth  29252  numclwwlkqhash  29382  isgrpo  29502  hvsubaddi  30071  hire  30099  shmodsi  30394  omlsilem  30407  chcon1i  30470  chnlei  30490  pjoml3i  30591  cmbr2i  30601  chscllem2  30643  adjsym  30838  eigorthi  30842  dfadj2  30890  adjval2  30896  cnvadj  30897  dmadjrnb  30911  adjvalval  30942  cnlnadjeui  31082  cnlnssadj  31085  adjbdln  31088  pjimai  31181  pjin2i  31198  pjin3i  31199  stadd3i  31253  largei  31272  cvnbtwn3  31293  cvnbtwn4  31294  mddmd2  31314  superpos  31359  atnemeq0  31382  sumdmdii  31420  sumdmdlem  31423  addltmulALT  31451  opreu2reuALT  31469  foresf1o  31495  difeq  31509  disjrdx  31576  fcoinvbr  31593  fmptco1f1o  31614  dfimafnf  31617  funcnvmpt  31650  curry2ima  31690  intimafv  31692  cnvoprabOLD  31705  elicoelioo  31749  wrdt2ind  31877  swrdrn3  31879  orngsqr  32170  qusker  32212  eqg0el  32221  lsmsnorb  32245  zarcls  32544  xrmulc1cn  32600  xrge0iifcnv  32603  ind1a  32707  esumfsup  32758  esumpcvgval  32766  esumcvg  32774  esum2dlem  32780  issgon  32811  eulerpartgbij  33061  eulerpartlemgh  33067  ballotlemsima  33204  bnj1366  33530  bnj553  33599  bnj964  33644  cusgredgex  33802  revwlk  33805  loop1cycl  33818  subfacp1lem3  33863  subfacp1lem5  33865  erdszelem9  33880  prv1n  34112  quad3  34345  br6  34416  elintfv  34425  dfon2lem5  34448  dfon2lem8  34451  brbigcup  34559  dfbigcup2  34560  elfix  34564  ellimits  34571  snelsingles  34583  dfiota3  34584  imageval  34591  brapply  34599  brsuccf  34602  funpartlem  34603  brfullfun  34609  dfrecs2  34611  dfrdg4  34612  altopthbg  34629  altopthc  34632  altopthd  34633  altopelaltxp  34637  brsegle  34769  outsideofrflx  34788  elicc3  34865  nn0prpw  34871  opnregcld  34878  cldregopn  34879  fneval  34900  topfneec  34903  knoppndvlem9  35059  bj-elgab  35482  bj-gabima  35483  bj-elsngl  35512  bj-snglc  35513  bj-projval  35540  bj-disj2r  35572  bj-restreg  35643  bj-0int  35645  copsex2b  35684  bj-inftyexpitaudisj  35749  bj-inftyexpidisj  35754  bj-bary1lem1  35855  topdifinffinlem  35891  topdifinfeq  35894  fvineqsnf1  35954  curf  36129  uncf  36130  curunc  36133  unccur  36134  poimirlem2  36153  poimirlem16  36167  poimirlem17  36168  poimirlem19  36170  poimirlem20  36171  poimirlem27  36178  mblfinlem2  36189  mbfresfi  36197  itg2addnclem2  36203  ftc1anclem3  36226  fdc  36277  heibor1  36342  opidonOLD  36384  0rngo  36559  smprngopr  36584  isfldidl  36600  isfldidl2  36601  eqbrb  36763  eqelb  36765  ideq2  36841  relcnveq  36856  n0elqs  36860  disjressuc2  36923  elrelscnveq  37027  disjdmqscossss  37338  lcvnbtwn3  37563  lcvexchlem1  37569  lsatnem0  37580  opcon1b  37733  omllaw2N  37779  cmtbr2N  37788  leatb  37827  cvlsupr2  37878  glbconxN  37914  islln3  38046  llnexatN  38057  islpln3  38069  lplnexatN  38099  islvol3  38112  dalem-cly  38207  isline4N  38313  2llnma3r  38324  poml4N  38489  4atex2  38613  4atex2-0bOLDN  38615  cdlemefrs29bpre0  38932  cdlemftr3  39101  cdlemb3  39142  cdlemg17h  39204  cdlemg17pq  39208  cdlemg19  39220  cdlemg21  39222  tendoex  39511  dva1dim  39521  dihglb2  39878  doch11  39909  dochsordN  39910  lcfrlem9  40086  hlhillcs  40498  lcmineqlem4  40562  metakunt1  40650  metakunt6  40655  metakunt15  40664  metakunt16  40665  fsuppind  40823  addsubeq4com  40852  elrfirn  41076  isnacs2  41087  isnacs3  41091  fiphp3d  41200  wopprc  41412  islnm2  41463  kercvrlsm  41468  fgraphopab  41595  tfsconcatlem  41729  tfsconcatrn  41735  tfsconcat0i  41738  tfsconcat0b  41739  tfsconcatrev  41741  oaun3lem1  41767  oadif1lem  41772  oadif1  41773  rp-fakeuninass  41910  snen1g  41918  iscard4  41927  sqrtcval  42035  frege124d  42155  frege129d  42157  frege92  42349  dffrege99  42356  clsk3nimkb  42434  clsk1indlem4  42438  clsk1indlem1  42439  ntrclsiso  42461  ntrclsk3  42464  ntrclsk13  42465  ntrneik4w  42494  extoimad  42559  int-sqdefd  42576  int-sqgeq0d  42581  radcnvrat  42716  bcc0  42742  opelopab4  42955  eqsbc2VD  43244  fzisoeu  43655  iuneqfzuz  43690  supxrleubrnmptf  43806  rexanuz2nf  43848  fsummulc1f  43932  fsumiunss  43936  fmul01lt1lem2  43946  sumnnodd  43991  fnlimfvre2  44038  limsupreuz  44098  limsupvaluz2  44099  liminfvalxr  44144  icccncfext  44248  cncfiooicc  44255  cncfioobdlem  44257  dvmptmulf  44298  dvmptfprodlem  44305  volioc  44333  itgioocnicc  44338  fourierdlem12  44480  fourierdlem20  44488  fourierdlem25  44493  fourierdlem33  44501  fourierdlem42  44510  fourierdlem52  44519  fourierdlem54  44521  fourierdlem57  44524  fourierdlem58  44525  fourierdlem59  44526  fourierdlem63  44530  fourierdlem65  44532  fourierdlem68  44535  fourierdlem73  44540  fourierdlem74  44541  fourierdlem75  44542  fourierdlem80  44547  fourierdlem81  44548  rrndistlt  44651  sge0ltfirpmpt2  44787  sge0pnfmpt  44806  hoidmv1le  44955  hoidmvle  44961  vonioolem2  45042  smflimlem3  45134  euabsneu  45382  funressnfv  45397  aiotaval  45447  reuf1odnf  45459  reuf1od  45460  afvpcfv0  45498  dfafn5a  45512  afvelrnb  45515  afvelrnb0  45516  dfaimafn2  45518  dfatsnafv2  45604  dfatdmfcoafv2  45606  f1oresf1o2  45643  0nelsetpreimafv  45702  fargshiftfo  45754  sprsymrelf1  45808  reupr  45834  fmtnorec2lem  45854  fmtnoprmfac1  45877  fmtnoprmfac2  45879  sfprmdvdsmersenne  45915  lighneallem2  45918  dfeven2  45961  dfodd3  45962  odd2np1ALTV  45986  even3prm2  46031  fppr2odd  46043  nnsum3primesgbe  46104  nnsum3primesle9  46106  isomuspgrlem2d  46143  0nodd  46224  2nodd  46226  lmod0rng  46286  rngcinv  46399  rngcinvALTV  46411  ringcinv  46450  ringcinvALTV  46474  lcoel0  46629  lindslinindimp2lem4  46662  ldepspr  46674  lincresunit3  46682  nn0sumshdiglemB  46826  nn0sumshdiglem1  46827  rrx2pnedifcoorneorr  46923  eenglngeehlnmlem1  46943  eenglngeehlnmlem2  46944  rrx2linest  46948  rrx2linest2  46950  rrxsphere  46954  line2ylem  46957  line2x  46960  itscnhlc0xyqsol  46971  itschlc0xyqsol1  46972  itsclinecirc0b  46980  2itscp  46987  inlinecirc02plem  46992