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 209	1 ⊢ (𝐴 = 𝐵 ↔ 𝐵 = 𝐴)

Syntax hints:   ↔ wb 206   = wceq 1541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2723

This theorem is referenced by:  eqcoms  2739  eqcomi  2740  neqcomd  2741  eqeq2d  2742  eqabcbw  2805  eqabcb  2872  necom  2981  nesym  2984  gencbvex  3495  clel5  3615  eqsbc2  3800  dfss  3916  sspsstri  4050  ssnelpss  4059  ssdifim  4218  disj4  4404  reuprg0  4650  preq1b  4793  invdisj  5072  disjprg  5082  dtruALT  5321  reusv3  5338  opthg2  5414  copsex2g  5428  copsex4g  5430  opcom  5436  opeqsng  5438  opeqpr  5440  snopeqop  5441  propeqop  5442  opthwiener  5449  vopelopabsb  5464  opthprc  5675  elxp3  5677  relop  5785  dmopab3  5854  rnopab3  5891  rncoeq  5916  restidsing  5997  somin1  6075  xpcan  6118  xpcan2  6119  dfrel4v  6132  dmsnn0  6149  reu3op  6234  reuop  6235  opreu2reurex  6236  ordtri2  6336  ordtri2or3  6403  suc11  6410  on0eqel  6426  snsn0non  6427  iota1  6455  iotan0  6466  sniota  6467  mptfnf  6611  fresaunres1  6691  dffn5  6875  fvelrnb  6877  dfimafn2  6880  funimass4  6881  feqmptdf  6887  fnsnfv  6896  dmfco  6913  fndmdif  6970  fneqeql  6974  rexrn  7015  ralrn  7016  elrnrexdmb  7018  dffo4  7031  fssrescdmd  7054  funopsn  7076  ftpg  7084  fprb  7123  ralima  7166  reximaOLD  7168  ralimaOLD  7169  fvclss  7170  dff13  7183  f1eqcocnv  7230  fnssintima  7291  imaeqsexvOLD  7292  riotaeqimp  7324  eusvobj2  7333  f1ocnvfv3  7336  oprabidw  7372  oprabid  7373  oprabv  7401  eloprabga  7450  ovelimab  7519  onmindif2  7735  br1steqg  7938  br2ndeqg  7939  dfoprab3  7981  opiota  7986  f1o2ndf1  8047  soseq  8084  brtpos2  8157  tpossym  8183  mpocurryd  8194  rdglim2  8346  tz7.48lem  8355  oaf1o  8473  omopthi  8571  erth2  8672  brecop  8729  erovlem  8732  ecopovsym  8738  eceqoveq  8741  xpcomco  8975  omxpenlem  8986  mapen  9049  nneneq  9110  unxpdomlem3  9137  unfilem1  9184  mapfien  9287  supgtoreq  9350  wemapsolem  9431  suc11reg  9504  inf3lem2  9514  inf3lem6  9518  ttrcltr  9601  djulf1o  9800  djurf1o  9801  infenaleph  9977  isinfcard  9978  dfac5  10015  cfeq0  10142  cfsuc  10143  ssfin4  10196  fin23lem25  10210  fin23lem22  10213  fin23lem40  10237  fin1a2lem5  10290  axcclem  10343  brdom7disj  10417  brdom6disj  10418  inar1  10661  psslinpr  10917  ltexprlem4  10925  ltsrpr  10963  mulgt0sr  10991  elreal  11017  ltresr  11026  leloe  11194  eqlei2  11219  addsubeq4  11370  subcan2  11381  negcon1  11408  negcon2  11409  addid0  11531  addeq0  11535  divmul2  11775  conjmul  11833  rereccl  11834  creur  12114  creui  12115  nndiv  12166  nn0sub  12426  elnn0z  12476  elznn0  12478  xrleloe  13038  ngtmnft  13060  icoshftf1o  13369  iccf1o  13391  fzen  13436  fzneuz  13503  injresinj  13686  fleqceilz  13753  mod0  13775  modmuladdnn0  13817  modirr  13844  addmodlteq  13848  nn0ennn  13881  hashrabsn01  14275  hashsdom  14283  hashgt12el2  14325  hashbclem  14354  hashfacen  14356  hashf1lem1  14357  hashtpg  14387  tpf1o  14403  fi1uzind  14409  ccatw2s1p1  14539  wrd2ind  14625  cshw1  14724  cshwsexa  14726  scshwfzeqfzo  14728  s2f1o  14818  wwlktovfo  14860  dmtrclfv  14920  cjreb  15025  leabs  15201  reusq0  15367  incexc2  15740  rpnnen2lem12  16129  dvdsval2  16161  dvdsabseq  16219  dvdsflip  16223  odd2np1  16247  oddm1even  16249  sqoddm1div8z  16260  m1exp1  16282  divalglem4  16302  divalglem8  16306  divalgb  16310  modremain  16314  zeqzmulgcd  16416  dfgcd2  16452  lcmfpr  16533  lcmftp  16542  lcmfunsnlem2  16546  divgcdcoprm0  16571  prm2orodd  16597  hashdvds  16681  oddprmdvds  16810  vdwlem12  16899  cshwshashlem1  17002  cshwsiun  17006  initoid  17903  termoid  17904  setcinv  17992  yonedainv  18182  joinfval  18272  joinfval2  18273  meetfval  18286  meetfval2  18287  latnle  18374  chnfi  18535  sgrp2nmndlem3  18828  grpid  18883  grpinvcnv  18914  grplmulf1o  18921  grpraddf1o  18922  grpsubeq0  18934  grpsubadd  18936  grplactcnv  18951  ressmulgnnd  18986  isnsg4  19074  eqg0el  19090  cycsubmel  19107  conjghm  19156  conjnmzb  19160  gacan  19212  gapm  19213  cntzrec  19243  oppgcntz  19271  fvcosymgeq  19336  odmulgeq  19464  dfod2  19471  sylow3lem3  19536  sylow3lem6  19539  lssnle  19581  lsmhash  19612  efgredlemb  19653  efgrelexlemb  19657  dprd2d2  19953  ablfac1eulem  19981  pgpfac1lem2  19984  pgpfac1lem4  19987  dvdsrval  20274  dvdsr02  20285  01eq0ring  20440  0ring01eqbi  20442  rngcinv  20547  ringcinv  20581  orngsqr  20776  rmodislmodlem  20857  lvecinv  21045  rngqiprngimf1lem  21226  rspsn  21265  dfcnfldOLD  21302  prmirredlem  21404  zndvds  21481  znleval  21486  psrbagconf1o  21861  mplmonmul  21966  gsummoncoe1  22218  evl1maprhm  22289  mat1dimelbas  22381  mat1dimbas  22382  1mavmul  22458  ma1repveval  22481  mulmarep1gsum1  22483  mdetunilem9  22530  m2cpminvid2lem  22664  pmatcollpw3lem  22693  mp2pm2mplem4  22719  toponsspwpw  22832  dmtopon  22833  cmpfi  23318  ssref  23422  qtopeu  23626  hmeoimaf1o  23680  txhmeo  23713  fbasrn  23794  rnelfmlem  23862  hauspwpwf1  23897  alexsubALTlem4  23960  qustgpopn  24030  qustgphaus  24033  fmucndlem  24200  isngp3  24508  isngp4  24522  metnrmlem1a  24769  icopnfcnv  24862  iccpnfcnv  24864  ivthle  25379  ivthle2  25380  dyadmbl  25523  mbfinf  25588  i1fmulclem  25625  itg1mulc  25627  mvth  25919  dvivth  25937  lhop2  25942  r1pid2  26089  dvdsq1p  26090  reeff1o  26379  coseq1  26456  recosf1o  26466  resinf1o  26467  efopn  26589  cxpeq  26689  logreclem  26694  affineequiv  26755  affineequiv4  26758  affineequivne  26759  quad2  26771  dcubic  26778  mcubic  26779  quart  26793  atandm2  26809  rlimcnp2  26898  amgm  26923  wilthlem2  27001  mumullem2  27112  sqff1o  27114  dvdsflf1o  27119  gausslemma2dlem0i  27297  lgseisenlem2  27309  lgsquadlem2  27314  2lgslem1c  27326  2lgsoddprmlem2  27342  2lgsoddprm  27349  2sq2  27366  addsq2reu  27373  2sqreultlem  27380  2sqreunnltlem  27383  2sqreulem3  27386  sltval2  27590  sltintdifex  27595  sltres  27596  nosepon  27599  noextenddif  27602  nosepssdm  27620  nogt01o  27630  nosupprefixmo  27634  noinfprefixmo  27635  nosupno  27637  noinfno  27652  sleloe  27688  eqscut2  27742  scutbdaylt  27754  elold  27809  made0  27813  lrrecfr  27881  subadds  28005  onscutlt  28196  zs12ge0  28388  renegscl  28395  tgjustf  28446  legtrid  28564  legso  28572  islmib  28760  lmicom  28761  lmiinv  28765  lmimid  28767  lmiopp  28775  colinearalglem2  28880  colinearalg  28883  ax5seglem4  28905  ax5seglem5  28906  axlowdimlem13  28927  axeuclidlem  28935  axeuclid  28936  axcontlem2  28938  axcontlem4  28940  elntg2  28958  structiedg0val  28995  uspgredgiedg  29148  uspgriedgedg  29149  usgredgsscusgredg  29433  fusgrn0degnn0  29473  umgr2v2evtxel  29496  vdiscusgrb  29504  uspgr2wlkeq  29619  wlk0prc  29626  wlklenvclwlk  29627  wlkp1lem8  29652  spthdep  29707  usgr2pthlem  29736  usgr2pth  29737  wlkiswwlksupgr2  29850  wlklnwwlkln2lem  29855  wwlksnextproplem3  29884  umgr2adedgwlk  29918  umgr2adedgspth  29921  umgr2wlkon  29923  umgrwwlks2on  29930  elwwlks2  29939  elwspths2spth  29940  clwlkclwwlklem2a4  29969  clwlkclwwlklem2  29972  erclwwlkref  29992  clwwlkf  30019  erclwwlknref  30041  erclwwlknsym  30042  erclwwlkntr  30043  hashecclwwlkn1  30049  umgrhashecclwwlk  30050  eupth2lem2  30191  eucrct2eupth  30217  numclwwlkqhash  30347  isgrpo  30469  hvsubaddi  31038  hire  31066  shmodsi  31361  omlsilem  31374  chcon1i  31437  chnlei  31457  pjoml3i  31558  cmbr2i  31568  chscllem2  31610  adjsym  31805  eigorthi  31809  dfadj2  31857  adjval2  31863  cnvadj  31864  dmadjrnb  31878  adjvalval  31909  cnlnadjeui  32049  cnlnssadj  32052  adjbdln  32055  pjimai  32148  pjin2i  32165  pjin3i  32166  stadd3i  32220  largei  32239  cvnbtwn3  32260  cvnbtwn4  32261  mddmd2  32281  superpos  32326  atnemeq0  32349  sumdmdii  32387  sumdmdlem  32390  addltmulALT  32418  opreu2reuALT  32448  foresf1o  32476  difeq  32490  disjrdx  32563  fcoinvbr  32577  brab2d  32580  fmptco1f1o  32607  dfimafnf  32610  funcnvmpt  32641  curry2ima  32682  intimafv  32684  receqid  32720  elicoelioo  32753  fzo0opth  32777  ind1a  32832  wrdt2ind  32926  swrdrn3  32928  cntrval2  33132  qusker  33306  dvdsrspss  33344  lsmsnorb  33348  1arithufdlem4  33504  r1pid2OLD  33561  algextdeglem8  33729  zarcls  33879  xrmulc1cn  33935  xrge0iifcnv  33938  esumfsup  34075  esumpcvgval  34083  esumcvg  34091  esum2dlem  34097  issgon  34128  eulerpartgbij  34377  eulerpartlemgh  34383  ballotlemsima  34521  bnj1366  34833  bnj553  34902  bnj964  34947  fineqvnttrclse  35136  cusgredgex  35158  revwlk  35161  loop1cycl  35173  subfacp1lem3  35218  subfacp1lem5  35220  erdszelem9  35235  prv1n  35467  ply1divalg3  35678  quad3  35706  br6  35793  elintfv  35801  dfon2lem5  35821  dfon2lem8  35824  brbigcup  35932  dfbigcup2  35933  elfix  35937  ellimits  35944  snelsingles  35956  dfiota3  35957  imageval  35964  brapply  35972  brsuccf  35975  funpartlem  35976  brfullfun  35982  dfrecs2  35984  dfrdg4  35985  altopthbg  36002  altopthc  36005  altopthd  36006  altopelaltxp  36010  brsegle  36142  outsideofrflx  36161  elicc3  36351  nn0prpw  36357  opnregcld  36364  cldregopn  36365  fneval  36386  topfneec  36389  knoppndvlem9  36554  bj-elgab  36973  bj-gabima  36974  bj-elsngl  37002  bj-snglc  37003  bj-projval  37030  bj-disj2r  37062  bj-restreg  37133  bj-0int  37135  copsex2b  37174  bj-inftyexpitaudisj  37239  bj-inftyexpidisj  37244  bj-bary1lem1  37345  topdifinffinlem  37381  topdifinfeq  37384  fvineqsnf1  37444  curf  37638  uncf  37639  curunc  37642  unccur  37643  poimirlem2  37662  poimirlem16  37676  poimirlem17  37677  poimirlem19  37679  poimirlem20  37680  poimirlem27  37687  mblfinlem2  37698  mbfresfi  37706  itg2addnclem2  37712  ftc1anclem3  37735  fdc  37785  heibor1  37850  opidonOLD  37892  0rngo  38067  smprngopr  38092  isfldidl  38108  isfldidl2  38109  eqbrb  38267  eqelb  38269  ideq2  38341  relcnveq  38356  n0elqs  38360  disjressuc2  38420  elrelscnveq  38529  qseq  38686  disjdmqscossss  38841  lcvnbtwn3  39067  lcvexchlem1  39073  lsatnem0  39084  opcon1b  39237  omllaw2N  39283  cmtbr2N  39292  leatb  39331  cvlsupr2  39382  glbconxN  39417  islln3  39549  llnexatN  39560  islpln3  39572  lplnexatN  39602  islvol3  39615  dalem-cly  39710  isline4N  39816  2llnma3r  39827  poml4N  39992  4atex2  40116  4atex2-0bOLDN  40118  cdlemefrs29bpre0  40435  cdlemftr3  40604  cdlemb3  40645  cdlemg17h  40707  cdlemg17pq  40711  cdlemg19  40723  cdlemg21  40725  tendoex  41014  dva1dim  41024  dihglb2  41381  doch11  41412  dochsordN  41413  lcfrlem9  41589  hlhillcs  41997  lcmineqlem4  42065  aks6d1c7lem2  42214  aks5lem3a  42222  aks5lem6  42225  unitscyglem2  42229  unitscyglem3  42230  addsubeq4com  42313  ef11d  42372  fimgmcyclem  42566  fsuppind  42623  elrfirn  42728  isnacs2  42739  isnacs3  42743  fiphp3d  42852  wopprc  43063  islnm2  43111  kercvrlsm  43116  fgraphopab  43236  tfsconcatlem  43369  tfsconcatrn  43375  tfsconcat0i  43378  tfsconcat0b  43379  tfsconcatrev  43381  oaun3lem1  43407  oadif1lem  43412  oadif1  43413  rp-fakeuninass  43549  snen1g  43557  iscard4  43566  sqrtcval  43674  frege124d  43794  frege129d  43796  frege92  43988  dffrege99  43995  clsk3nimkb  44073  clsk1indlem4  44077  clsk1indlem1  44078  ntrclsiso  44100  ntrclsk3  44103  ntrclsk13  44104  ntrneik4w  44133  extoimad  44197  int-sqdefd  44214  int-sqgeq0d  44219  radcnvrat  44347  bcc0  44373  opelopab4  44584  eqsbc2VD  44872  fzisoeu  45341  iuneqfzuz  45374  supxrleubrnmptf  45489  rexanuz2nf  45530  fsummulc1f  45611  fsumiunss  45615  fmul01lt1lem2  45625  sumnnodd  45670  fnlimfvre2  45715  limsupreuz  45775  limsupvaluz2  45776  liminfvalxr  45821  icccncfext  45925  cncfiooicc  45932  cncfioobdlem  45934  dvmptmulf  45975  dvmptfprodlem  45982  volioc  46010  itgioocnicc  46015  fourierdlem12  46157  fourierdlem20  46165  fourierdlem25  46170  fourierdlem33  46178  fourierdlem42  46187  fourierdlem52  46196  fourierdlem54  46198  fourierdlem57  46201  fourierdlem58  46202  fourierdlem59  46203  fourierdlem63  46207  fourierdlem65  46209  fourierdlem68  46212  fourierdlem73  46217  fourierdlem74  46218  fourierdlem75  46219  fourierdlem80  46224  fourierdlem81  46225  rrndistlt  46328  sge0ltfirpmpt2  46464  sge0pnfmpt  46483  hoidmv1le  46632  hoidmvle  46638  vonioolem2  46719  smflimlem3  46811  lambert0  46918  lamberte  46919  euabsneu  47059  funressnfv  47074  aiotaval  47126  reuf1odnf  47138  reuf1od  47139  afvpcfv0  47177  dfafn5a  47191  afvelrnb  47194  afvelrnb0  47195  dfaimafn2  47197  dfatsnafv2  47283  dfatdmfcoafv2  47285  f1oresf1o2  47322  ceilbi  47364  minusmodnep2tmod  47384  0nelsetpreimafv  47421  fargshiftfo  47473  sprsymrelf1  47527  reupr  47553  fmtnorec2lem  47573  fmtnoprmfac1  47596  fmtnoprmfac2  47598  sfprmdvdsmersenne  47634  lighneallem2  47637  dfeven2  47680  dfodd3  47681  odd2np1ALTV  47705  even3prm2  47750  fppr2odd  47762  nnsum3primesgbe  47823  nnsum3primesle9  47825  clnbgrsym  47869  dfvopnbgr2  47884  isuspgrim0  47925  isuspgrimlem  47926  dfgric2  47946  grtriprop  47972  uspgrlimlem3  48021  gpgvtxedg1  48095  pgnbgreunbgrlem2lem1  48145  pgnbgreunbgrlem2lem2  48146  0nodd  48201  2nodd  48203  lmod0rng  48260  rngcinvALTV  48307  ringcinvALTV  48341  lcoel0  48460  lindslinindimp2lem4  48493  ldepspr  48505  lincresunit3  48513  nn0sumshdiglemB  48652  nn0sumshdiglem1  48653  rrx2pnedifcoorneorr  48749  eenglngeehlnmlem1  48769  eenglngeehlnmlem2  48770  rrx2linest  48774  rrx2linest2  48776  rrxsphere  48780  line2ylem  48783  line2x  48786  itscnhlc0xyqsol  48797  itschlc0xyqsol1  48798  itsclinecirc0b  48806  2itscp  48813  inlinecirc02plem  48818  brab2dd  48859  uptr2  49253