Theorem eqcom 2740

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 2739	. 2 ⊢ (𝐴 = 𝐵 → 𝐵 = 𝐴)
3		id 22	. . 3 ⊢ (𝐵 = 𝐴 → 𝐵 = 𝐴)
4	3	eqcomd 2739	. 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 2123  ax-ext 2705

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

This theorem is referenced by:  eqcoms  2741  eqcomi  2742  neqcomd  2743  eqeq2d  2744  eqabcbw  2807  eqabcb  2873  necom  2982  nesym  2985  gencbvex  3496  clel5  3616  eqsbc2  3801  dfss  3917  sspsstri  4054  ssnelpss  4063  ssdifim  4222  disj4  4408  reuprg0  4656  preq1b  4799  invdisj  5081  disjprg  5091  dtruALT  5330  reusv3  5347  opthg2  5424  copsex2g  5438  copsex4g  5440  opcom  5446  opeqsng  5448  opeqpr  5450  snopeqop  5451  propeqop  5452  opthwiener  5459  vopelopabsb  5474  opthprc  5685  elxp3  5687  relop  5796  dmopab3  5865  rnopab3  5902  rncoeq  5928  restidsing  6009  somin1  6087  xpcan  6131  xpcan2  6132  dfrel4v  6145  dmsnn0  6162  reu3op  6247  reuop  6248  opreu2reurex  6249  ordtri2  6349  ordtri2or3  6416  suc11  6423  on0eqel  6439  snsn0non  6440  iota1  6468  iotan0  6479  sniota  6480  mptfnf  6624  fresaunres1  6704  dffn5  6889  fvelrnb  6891  dfimafn2  6894  funimass4  6895  feqmptdf  6901  fnsnfv  6910  dmfco  6927  fndmdif  6984  fneqeql  6988  rexrn  7029  ralrn  7030  elrnrexdmb  7032  dffo4  7045  fssrescdmd  7068  funopsn  7090  ftpg  7098  fprb  7137  ralima  7180  reximaOLD  7182  ralimaOLD  7183  fvclss  7184  dff13  7197  f1eqcocnv  7244  fnssintima  7305  imaeqsexvOLD  7306  riotaeqimp  7338  eusvobj2  7347  f1ocnvfv3  7350  oprabidw  7386  oprabid  7387  oprabv  7415  eloprabga  7464  ovelimab  7533  onmindif2  7749  br1steqg  7952  br2ndeqg  7953  dfoprab3  7995  opiota  8000  f1o2ndf1  8061  soseq  8098  brtpos2  8171  tpossym  8197  mpocurryd  8208  rdglim2  8360  tz7.48lem  8369  oaf1o  8487  omopthi  8585  erth2  8686  brecop  8743  erovlem  8746  ecopovsym  8752  eceqoveq  8755  xpcomco  8991  omxpenlem  9002  mapen  9065  nneneq  9126  unxpdomlem3  9153  unfilem1  9200  mapfien  9303  supgtoreq  9366  wemapsolem  9447  suc11reg  9520  inf3lem2  9530  inf3lem6  9534  ttrcltr  9617  djulf1o  9816  djurf1o  9817  infenaleph  9993  isinfcard  9994  dfac5  10031  cfeq0  10158  cfsuc  10159  ssfin4  10212  fin23lem25  10226  fin23lem22  10229  fin23lem40  10253  fin1a2lem5  10306  axcclem  10359  brdom7disj  10433  brdom6disj  10434  inar1  10677  psslinpr  10933  ltexprlem4  10941  ltsrpr  10979  mulgt0sr  11007  elreal  11033  ltresr  11042  leloe  11210  eqlei2  11235  addsubeq4  11386  subcan2  11397  negcon1  11424  negcon2  11425  addid0  11547  addeq0  11551  divmul2  11791  conjmul  11849  rereccl  11850  creur  12130  creui  12131  nndiv  12182  nn0sub  12442  elnn0z  12492  elznn0  12494  xrleloe  13049  ngtmnft  13072  icoshftf1o  13381  iccf1o  13403  fzen  13448  fzneuz  13515  injresinj  13698  fleqceilz  13765  mod0  13787  modmuladdnn0  13829  modirr  13856  addmodlteq  13860  nn0ennn  13893  hashrabsn01  14287  hashsdom  14295  hashgt12el2  14337  hashbclem  14366  hashfacen  14368  hashf1lem1  14369  hashtpg  14399  tpf1o  14415  fi1uzind  14421  ccatw2s1p1  14551  wrd2ind  14637  cshw1  14736  cshwsexa  14738  scshwfzeqfzo  14740  s2f1o  14830  wwlktovfo  14872  dmtrclfv  14932  cjreb  15037  leabs  15213  reusq0  15379  incexc2  15752  rpnnen2lem12  16141  dvdsval2  16173  dvdsabseq  16231  dvdsflip  16235  odd2np1  16259  oddm1even  16261  sqoddm1div8z  16272  m1exp1  16294  divalglem4  16314  divalglem8  16318  divalgb  16322  modremain  16326  zeqzmulgcd  16428  dfgcd2  16464  lcmfpr  16545  lcmftp  16554  lcmfunsnlem2  16558  divgcdcoprm0  16583  prm2orodd  16609  hashdvds  16693  oddprmdvds  16822  vdwlem12  16911  cshwshashlem1  17014  cshwsiun  17018  initoid  17916  termoid  17917  setcinv  18005  yonedainv  18195  joinfval  18285  joinfval2  18286  meetfval  18299  meetfval2  18300  latnle  18387  chnfi  18548  sgrp2nmndlem3  18841  grpid  18896  grpinvcnv  18927  grplmulf1o  18934  grpraddf1o  18935  grpsubeq0  18947  grpsubadd  18949  grplactcnv  18964  ressmulgnnd  18999  isnsg4  19087  eqg0el  19103  cycsubmel  19120  conjghm  19169  conjnmzb  19173  gacan  19225  gapm  19226  cntzrec  19256  oppgcntz  19284  fvcosymgeq  19349  odmulgeq  19477  dfod2  19484  sylow3lem3  19549  sylow3lem6  19552  lssnle  19594  lsmhash  19625  efgredlemb  19666  efgrelexlemb  19670  dprd2d2  19966  ablfac1eulem  19994  pgpfac1lem2  19997  pgpfac1lem4  20000  dvdsrval  20288  dvdsr02  20299  01eq0ring  20454  0ring01eqbi  20456  rngcinv  20561  ringcinv  20595  orngsqr  20790  rmodislmodlem  20871  lvecinv  21059  rngqiprngimf1lem  21240  rspsn  21279  dfcnfldOLD  21316  prmirredlem  21418  zndvds  21495  znleval  21500  psrbagconf1o  21876  mplmonmul  21982  gsummoncoe1  22243  evl1maprhm  22314  mat1dimelbas  22406  mat1dimbas  22407  1mavmul  22483  ma1repveval  22506  mulmarep1gsum1  22508  mdetunilem9  22555  m2cpminvid2lem  22689  pmatcollpw3lem  22718  mp2pm2mplem4  22744  toponsspwpw  22857  dmtopon  22858  cmpfi  23343  ssref  23447  qtopeu  23651  hmeoimaf1o  23705  txhmeo  23738  fbasrn  23819  rnelfmlem  23887  hauspwpwf1  23922  alexsubALTlem4  23985  qustgpopn  24055  qustgphaus  24058  fmucndlem  24225  isngp3  24533  isngp4  24547  metnrmlem1a  24794  icopnfcnv  24887  iccpnfcnv  24889  ivthle  25404  ivthle2  25405  dyadmbl  25548  mbfinf  25613  i1fmulclem  25650  itg1mulc  25652  mvth  25944  dvivth  25962  lhop2  25967  r1pid2  26114  dvdsq1p  26115  reeff1o  26404  coseq1  26481  recosf1o  26491  resinf1o  26492  efopn  26614  cxpeq  26714  logreclem  26719  affineequiv  26780  affineequiv4  26783  affineequivne  26784  quad2  26796  dcubic  26803  mcubic  26804  quart  26818  atandm2  26834  rlimcnp2  26923  amgm  26948  wilthlem2  27026  mumullem2  27137  sqff1o  27139  dvdsflf1o  27144  gausslemma2dlem0i  27322  lgseisenlem2  27334  lgsquadlem2  27339  2lgslem1c  27351  2lgsoddprmlem2  27367  2lgsoddprm  27374  2sq2  27391  addsq2reu  27398  2sqreultlem  27405  2sqreunnltlem  27408  2sqreulem3  27411  sltval2  27615  sltintdifex  27620  sltres  27621  nosepon  27624  noextenddif  27627  nosepssdm  27645  nogt01o  27655  nosupprefixmo  27659  noinfprefixmo  27660  nosupno  27662  noinfno  27677  sleloe  27713  eqscut2  27767  scutbdaylt  27779  elold  27834  made0  27838  lrrecfr  27906  subadds  28030  onscutlt  28221  zs12ge0  28413  renegscl  28420  tgjustf  28471  legtrid  28589  legso  28597  islmib  28785  lmicom  28786  lmiinv  28790  lmimid  28792  lmiopp  28800  colinearalglem2  28906  colinearalg  28909  ax5seglem4  28931  ax5seglem5  28932  axlowdimlem13  28953  axeuclidlem  28961  axeuclid  28962  axcontlem2  28964  axcontlem4  28966  elntg2  28984  structiedg0val  29021  uspgredgiedg  29174  uspgriedgedg  29175  usgredgsscusgredg  29459  fusgrn0degnn0  29499  umgr2v2evtxel  29522  vdiscusgrb  29530  uspgr2wlkeq  29645  wlk0prc  29652  wlklenvclwlk  29653  wlkp1lem8  29678  spthdep  29733  usgr2pthlem  29762  usgr2pth  29763  wlkiswwlksupgr2  29876  wlklnwwlkln2lem  29881  wwlksnextproplem3  29910  umgr2adedgwlk  29944  umgr2adedgspth  29947  umgr2wlkon  29949  usgrwwlks2on  29957  umgrwwlks2on  29958  elwwlks2  29968  elwspths2spth  29969  clwlkclwwlklem2a4  29998  clwlkclwwlklem2  30001  erclwwlkref  30021  clwwlkf  30048  erclwwlknref  30070  erclwwlknsym  30071  erclwwlkntr  30072  hashecclwwlkn1  30078  umgrhashecclwwlk  30079  eupth2lem2  30220  eucrct2eupth  30246  numclwwlkqhash  30376  isgrpo  30498  hvsubaddi  31067  hire  31095  shmodsi  31390  omlsilem  31403  chcon1i  31466  chnlei  31486  pjoml3i  31587  cmbr2i  31597  chscllem2  31639  adjsym  31834  eigorthi  31838  dfadj2  31886  adjval2  31892  cnvadj  31893  dmadjrnb  31907  adjvalval  31938  cnlnadjeui  32078  cnlnssadj  32081  adjbdln  32084  pjimai  32177  pjin2i  32194  pjin3i  32195  stadd3i  32249  largei  32268  cvnbtwn3  32289  cvnbtwn4  32290  mddmd2  32310  superpos  32355  atnemeq0  32378  sumdmdii  32416  sumdmdlem  32419  addltmulALT  32447  opreu2reuALT  32477  foresf1o  32505  difeq  32519  disjrdx  32592  fcoinvbr  32606  brab2d  32609  fmptco1f1o  32637  dfimafnf  32640  funcnvmpt  32671  curry2ima  32714  intimafv  32716  receqid  32752  elicoelioo  32786  fzo0opth  32811  ind1a  32866  wrdt2ind  32963  swrdrn3  32965  gsummptp1  33068  gsummulsubdishift1  33079  cntrval2  33181  domnprodeq0  33286  qusker  33358  dvdsrspss  33396  lsmsnorb  33400  1arithufdlem4  33556  r1pid2OLD  33618  esplyind  33659  algextdeglem8  33809  zarcls  33959  xrmulc1cn  34015  xrge0iifcnv  34018  esumfsup  34155  esumpcvgval  34163  esumcvg  34171  esum2dlem  34177  issgon  34208  eulerpartgbij  34457  eulerpartlemgh  34463  ballotlemsima  34601  bnj1366  34913  bnj553  34982  bnj964  35027  fineqvnttrclse  35216  cusgredgex  35238  revwlk  35241  loop1cycl  35253  subfacp1lem3  35298  subfacp1lem5  35300  erdszelem9  35315  prv1n  35547  ply1divalg3  35758  quad3  35786  br6  35873  elintfv  35881  dfon2lem5  35901  dfon2lem8  35904  brbigcup  36012  dfbigcup2  36013  elfix  36017  ellimits  36024  snelsingles  36036  dfiota3  36037  imageval  36044  brapply  36052  lemsuccf  36055  dfsuccf2  36057  funpartlem  36058  brfullfun  36064  dfrecs2  36066  dfrdg4  36067  altopthbg  36084  altopthc  36087  altopthd  36088  altopelaltxp  36092  brsegle  36224  outsideofrflx  36243  elicc3  36433  nn0prpw  36439  opnregcld  36446  cldregopn  36447  fneval  36468  topfneec  36471  knoppndvlem9  36636  bj-elgab  37056  bj-gabima  37057  bj-elsngl  37085  bj-snglc  37086  bj-projval  37113  bj-disj2r  37145  bj-restreg  37216  bj-0int  37218  copsex2b  37257  bj-inftyexpitaudisj  37322  bj-inftyexpidisj  37327  bj-bary1lem1  37428  topdifinffinlem  37464  topdifinfeq  37467  fvineqsnf1  37527  curf  37711  uncf  37712  curunc  37715  unccur  37716  poimirlem2  37735  poimirlem16  37749  poimirlem17  37750  poimirlem19  37752  poimirlem20  37753  poimirlem27  37760  mblfinlem2  37771  mbfresfi  37779  itg2addnclem2  37785  ftc1anclem3  37808  fdc  37858  heibor1  37923  opidonOLD  37965  0rngo  38140  smprngopr  38165  isfldidl  38181  isfldidl2  38182  eqbrb  38347  eqelb  38349  ideq2  38418  relcnveq  38433  n0elqs  38437  disjressuc2  38508  dfsucmap3  38549  dfsucmap4  38551  dmsucmap  38554  preuniqval  38581  elrelscnveq  38713  qseq  38819  disjdmqscossss  38974  lcvnbtwn3  39200  lcvexchlem1  39206  lsatnem0  39217  opcon1b  39370  omllaw2N  39416  cmtbr2N  39425  leatb  39464  cvlsupr2  39515  glbconxN  39550  islln3  39682  llnexatN  39693  islpln3  39705  lplnexatN  39735  islvol3  39748  dalem-cly  39843  isline4N  39949  2llnma3r  39960  poml4N  40125  4atex2  40249  4atex2-0bOLDN  40251  cdlemefrs29bpre0  40568  cdlemftr3  40737  cdlemb3  40778  cdlemg17h  40840  cdlemg17pq  40844  cdlemg19  40856  cdlemg21  40858  tendoex  41147  dva1dim  41157  dihglb2  41514  doch11  41545  dochsordN  41546  lcfrlem9  41722  hlhillcs  42130  lcmineqlem4  42198  aks6d1c7lem2  42347  aks5lem3a  42355  aks5lem6  42358  unitscyglem2  42362  unitscyglem3  42363  addsubeq4com  42450  ef11d  42509  fimgmcyclem  42703  fsuppind  42748  elrfirn  42852  isnacs2  42863  isnacs3  42867  fiphp3d  42976  wopprc  43187  islnm2  43235  kercvrlsm  43240  fgraphopab  43360  tfsconcatlem  43493  tfsconcatrn  43499  tfsconcat0i  43502  tfsconcat0b  43503  tfsconcatrev  43505  oaun3lem1  43531  oadif1lem  43536  oadif1  43537  rp-fakeuninass  43673  snen1g  43681  iscard4  43690  sqrtcval  43798  frege124d  43918  frege129d  43920  frege92  44112  dffrege99  44119  clsk3nimkb  44197  clsk1indlem4  44201  clsk1indlem1  44202  ntrclsiso  44224  ntrclsk3  44227  ntrclsk13  44228  ntrneik4w  44257  extoimad  44321  int-sqdefd  44338  int-sqgeq0d  44343  radcnvrat  44471  bcc0  44497  opelopab4  44708  eqsbc2VD  44996  fzisoeu  45464  iuneqfzuz  45496  supxrleubrnmptf  45611  rexanuz2nf  45652  fsummulc1f  45733  fsumiunss  45737  fmul01lt1lem2  45747  sumnnodd  45792  fnlimfvre2  45837  limsupreuz  45897  limsupvaluz2  45898  liminfvalxr  45943  icccncfext  46047  cncfiooicc  46054  cncfioobdlem  46056  dvmptmulf  46097  dvmptfprodlem  46104  volioc  46132  itgioocnicc  46137  fourierdlem12  46279  fourierdlem20  46287  fourierdlem25  46292  fourierdlem33  46300  fourierdlem42  46309  fourierdlem52  46318  fourierdlem54  46320  fourierdlem57  46323  fourierdlem58  46324  fourierdlem59  46325  fourierdlem63  46329  fourierdlem65  46331  fourierdlem68  46334  fourierdlem73  46339  fourierdlem74  46340  fourierdlem75  46341  fourierdlem80  46346  fourierdlem81  46347  rrndistlt  46450  sge0ltfirpmpt2  46586  sge0pnfmpt  46605  hoidmv1le  46754  hoidmvle  46760  vonioolem2  46841  smflimlem3  46933  chnsubseqwl  47039  lambert0  47049  lamberte  47050  euabsneu  47190  funressnfv  47205  aiotaval  47257  reuf1odnf  47269  reuf1od  47270  afvpcfv0  47308  dfafn5a  47322  afvelrnb  47325  afvelrnb0  47326  dfaimafn2  47328  dfatsnafv2  47414  dfatdmfcoafv2  47416  f1oresf1o2  47453  ceilbi  47495  minusmodnep2tmod  47515  0nelsetpreimafv  47552  fargshiftfo  47604  sprsymrelf1  47658  reupr  47684  fmtnorec2lem  47704  fmtnoprmfac1  47727  fmtnoprmfac2  47729  sfprmdvdsmersenne  47765  lighneallem2  47768  dfeven2  47811  dfodd3  47812  odd2np1ALTV  47836  even3prm2  47881  fppr2odd  47893  nnsum3primesgbe  47954  nnsum3primesle9  47956  clnbgrsym  48000  dfvopnbgr2  48015  isuspgrim0  48056  isuspgrimlem  48057  dfgric2  48077  grtriprop  48103  uspgrlimlem3  48152  gpgvtxedg1  48226  pgnbgreunbgrlem2lem1  48276  pgnbgreunbgrlem2lem2  48277  0nodd  48332  2nodd  48334  lmod0rng  48391  rngcinvALTV  48438  ringcinvALTV  48472  lcoel0  48590  lindslinindimp2lem4  48623  ldepspr  48635  lincresunit3  48643  nn0sumshdiglemB  48782  nn0sumshdiglem1  48783  rrx2pnedifcoorneorr  48879  eenglngeehlnmlem1  48899  eenglngeehlnmlem2  48900  rrx2linest  48904  rrx2linest2  48906  rrxsphere  48910  line2ylem  48913  line2x  48916  itscnhlc0xyqsol  48927  itschlc0xyqsol1  48928  itsclinecirc0b  48936  2itscp  48943  inlinecirc02plem  48948  brab2dd  48989  uptr2  49382