Theorem eqcom 2747

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

Syntax hints:   ↔ wb 206   = wceq 1537

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732

This theorem is referenced by:  eqcoms  2748  eqcomi  2749  neqcomd  2750  eqeq2d  2751  eqtr2OLD  2765  eqtr3OLD  2767  eqabcb  2886  necom  3000  nesym  3003  pm13.181OLD  3030  gencbvex  3553  clel5  3678  eqsbc2  3873  dfss  3995  sspsstri  4128  ssnelpss  4137  ssdifim  4292  disj  4473  disj4  4482  reuprg0  4727  preq1b  4871  invdisj  5152  disjprg  5162  dtruALT  5406  reusv3  5423  opthg2  5499  copsex2g  5513  copsex4g  5514  opcom  5520  opeqsng  5522  opeqpr  5524  snopeqop  5525  propeqop  5526  opthwiener  5533  vopelopabsb  5548  opthprc  5764  elxp3  5766  relop  5875  dmopab3  5944  rncoeq  6002  restidsing  6082  somin1  6165  xpcan  6207  xpcan2  6208  dfrel4v  6221  dmsnn0  6238  reu3op  6323  reuop  6324  opreu2reurex  6325  ordtri2  6430  ordtri2or3  6495  suc11  6502  on0eqel  6519  snsn0non  6520  iota1  6550  iotan0  6563  sniota  6564  mptfnf  6715  fresaunres1  6794  dffn5  6980  fvelrnb  6982  dfimafn2  6985  funimass4  6986  feqmptdf  6992  fnsnfv  7001  dmfco  7018  fndmdif  7075  fneqeql  7079  rexrn  7121  ralrn  7122  elrnrexdmb  7124  dffo4  7137  fssrescdmd  7160  funopsn  7182  ftpg  7190  fprb  7231  ralima  7274  reximaOLD  7276  ralimaOLD  7277  fvclss  7278  dff13  7292  f1eqcocnv  7337  fnssintima  7398  imaeqsexvOLD  7399  riotaeqimp  7431  eusvobj2  7440  f1ocnvfv3  7443  oprabidw  7479  oprabid  7480  oprabv  7510  eloprabga  7558  eloprabgaOLD  7559  ovelimab  7628  onmindif2  7843  br1steqg  8052  br2ndeqg  8053  dfoprab3  8095  opiota  8100  f1o2ndf1  8163  soseq  8200  brtpos2  8273  tpossym  8299  mpocurryd  8310  rdglim2  8488  tz7.48lem  8497  oaf1o  8619  omopthi  8717  erth2  8815  brecop  8868  erovlem  8871  ecopovsym  8877  eceqoveq  8880  xpcomco  9128  omxpenlem  9139  mapen  9207  nneneq  9272  nneneqOLD  9284  unxpdomlem3  9315  unfilem1  9371  mapfien  9477  supgtoreq  9539  wemapsolem  9619  suc11reg  9688  inf3lem2  9698  inf3lem6  9702  ttrcltr  9785  djulf1o  9981  djurf1o  9982  infenaleph  10160  isinfcard  10161  dfac5  10198  cfeq0  10325  cfsuc  10326  ssfin4  10379  fin23lem25  10393  fin23lem22  10396  fin23lem40  10420  fin1a2lem5  10473  axcclem  10526  brdom7disj  10600  brdom6disj  10601  inar1  10844  psslinpr  11100  ltexprlem4  11108  ltsrpr  11146  mulgt0sr  11174  elreal  11200  ltresr  11209  leloe  11376  eqlei2  11401  addsubeq4  11551  subcan2  11561  negcon1  11588  negcon2  11589  addid0  11709  addeq0  11713  divmul2  11953  conjmul  12011  rereccl  12012  creur  12287  creui  12288  nndiv  12339  nn0sub  12603  elnn0z  12652  elznn0  12654  xrleloe  13206  ngtmnft  13228  icoshftf1o  13534  iccf1o  13556  fzen  13601  fzneuz  13665  injresinj  13838  fleqceilz  13905  mod0  13927  modmuladdnn0  13966  modirr  13993  addmodlteq  13997  nn0ennn  14030  hashrabsn01  14422  hashsdom  14430  hashgt12el2  14472  hashbclem  14501  hashfacen  14503  hashf1lem1  14504  hashtpg  14534  tpf1o  14550  fi1uzind  14556  ccatw2s1p1  14684  wrd2ind  14771  cshw1  14870  cshwsexa  14872  scshwfzeqfzo  14875  s2f1o  14965  wwlktovfo  15007  dmtrclfv  15067  cjreb  15172  leabs  15348  reusq0  15511  incexc2  15886  rpnnen2lem12  16273  dvdsval2  16305  dvdsabseq  16361  dvdsflip  16365  odd2np1  16389  oddm1even  16391  sqoddm1div8z  16402  m1exp1  16424  divalglem4  16444  divalglem8  16448  divalgb  16452  modremain  16456  zeqzmulgcd  16556  dfgcd2  16593  lcmfpr  16674  lcmftp  16683  lcmfunsnlem2  16687  divgcdcoprm0  16712  prm2orodd  16738  hashdvds  16822  oddprmdvds  16950  vdwlem12  17039  cshwshashlem1  17143  cshwsiun  17147  initoid  18068  termoid  18069  setcinv  18157  yonedainv  18351  joinfval  18443  joinfval2  18444  meetfval  18457  meetfval2  18458  latnle  18543  sgrp2nmndlem3  18960  grpid  19015  grpinvcnv  19046  grplmulf1o  19053  grpraddf1o  19054  grpsubeq0  19066  grpsubadd  19068  grplactcnv  19083  ressmulgnnd  19118  isnsg4  19207  eqg0el  19223  cycsubmel  19240  conjghm  19289  conjnmzb  19293  gacan  19345  gapm  19346  cntzrec  19376  oppgcntz  19407  fvcosymgeq  19471  odmulgeq  19599  dfod2  19606  sylow3lem3  19671  sylow3lem6  19674  lssnle  19716  lsmhash  19747  efgredlemb  19788  efgrelexlemb  19792  dprd2d2  20088  ablfac1eulem  20116  pgpfac1lem2  20119  pgpfac1lem4  20122  dvdsrval  20387  dvdsr02  20398  01eq0ring  20556  0ring01eqbi  20558  rngcinv  20659  ringcinv  20693  rmodislmodlem  20949  lvecinv  21138  rngqiprngimf1lem  21327  rspsn  21366  dfcnfldOLD  21403  prmirredlem  21506  zndvds  21591  znleval  21596  psrbagconf1o  21972  mplmonmul  22077  gsummoncoe1  22333  evl1maprhm  22404  mat1dimelbas  22498  mat1dimbas  22499  1mavmul  22575  ma1repveval  22598  mulmarep1gsum1  22600  mdetunilem9  22647  m2cpminvid2lem  22781  pmatcollpw3lem  22810  mp2pm2mplem4  22836  toponsspwpw  22949  dmtopon  22950  cmpfi  23437  ssref  23541  qtopeu  23745  hmeoimaf1o  23799  txhmeo  23832  fbasrn  23913  rnelfmlem  23981  hauspwpwf1  24016  alexsubALTlem4  24079  qustgpopn  24149  qustgphaus  24152  fmucndlem  24321  isngp3  24632  isngp4  24646  metnrmlem1a  24899  icopnfcnv  24992  iccpnfcnv  24994  ivthle  25510  ivthle2  25511  dyadmbl  25654  mbfinf  25719  i1fmulclem  25757  itg1mulc  25759  mvth  26051  dvivth  26069  lhop2  26074  r1pid2  26221  dvdsq1p  26222  reeff1o  26509  coseq1  26585  recosf1o  26595  resinf1o  26596  efopn  26718  cxpeq  26818  logreclem  26823  affineequiv  26884  affineequiv4  26887  affineequivne  26888  quad2  26900  dcubic  26907  mcubic  26908  quart  26922  atandm2  26938  rlimcnp2  27027  amgm  27052  wilthlem2  27130  mumullem2  27241  sqff1o  27243  dvdsflf1o  27248  gausslemma2dlem0i  27426  lgseisenlem2  27438  lgsquadlem2  27443  2lgslem1c  27455  2lgsoddprmlem2  27471  2lgsoddprm  27478  2sq2  27495  addsq2reu  27502  2sqreultlem  27509  2sqreunnltlem  27512  2sqreulem3  27515  sltval2  27719  sltintdifex  27724  sltres  27725  nosepon  27728  noextenddif  27731  nosepssdm  27749  nogt01o  27759  nosupprefixmo  27763  noinfprefixmo  27764  nosupno  27766  noinfno  27781  sleloe  27817  eqscut2  27869  scutbdaylt  27881  elold  27926  made0  27930  lrrecfr  27994  subadds  28118  cutpw2  28435  renegscl  28448  tgjustf  28499  legtrid  28617  legso  28625  islmib  28813  lmicom  28814  lmiinv  28818  lmimid  28820  lmiopp  28828  colinearalglem2  28940  colinearalg  28943  ax5seglem4  28965  ax5seglem5  28966  axlowdimlem13  28987  axeuclidlem  28995  axeuclid  28996  axcontlem2  28998  axcontlem4  29000  elntg2  29018  structiedg0val  29057  uspgredgiedg  29210  uspgriedgedg  29211  usgredgsscusgredg  29495  fusgrn0degnn0  29535  umgr2v2evtxel  29558  vdiscusgrb  29566  uspgr2wlkeq  29682  wlk0prc  29690  wlklenvclwlk  29691  wlkp1lem8  29716  spthdep  29770  usgr2pthlem  29799  usgr2pth  29800  wlkiswwlksupgr2  29910  wlklnwwlkln2lem  29915  wwlksnextproplem3  29944  umgr2adedgwlk  29978  umgr2adedgspth  29981  umgr2wlkon  29983  umgrwwlks2on  29990  elwwlks2  29999  elwspths2spth  30000  clwlkclwwlklem2a4  30029  clwlkclwwlklem2  30032  erclwwlkref  30052  clwwlkf  30079  erclwwlknref  30101  erclwwlknsym  30102  erclwwlkntr  30103  hashecclwwlkn1  30109  umgrhashecclwwlk  30110  eupth2lem2  30251  eucrct2eupth  30277  numclwwlkqhash  30407  isgrpo  30529  hvsubaddi  31098  hire  31126  shmodsi  31421  omlsilem  31434  chcon1i  31497  chnlei  31517  pjoml3i  31618  cmbr2i  31628  chscllem2  31670  adjsym  31865  eigorthi  31869  dfadj2  31917  adjval2  31923  cnvadj  31924  dmadjrnb  31938  adjvalval  31969  cnlnadjeui  32109  cnlnssadj  32112  adjbdln  32115  pjimai  32208  pjin2i  32225  pjin3i  32226  stadd3i  32280  largei  32299  cvnbtwn3  32320  cvnbtwn4  32321  mddmd2  32341  superpos  32386  atnemeq0  32409  sumdmdii  32447  sumdmdlem  32450  addltmulALT  32478  opreu2reuALT  32505  foresf1o  32532  difeq  32548  disjrdx  32613  fcoinvbr  32627  brab2d  32629  fmptco1f1o  32652  dfimafnf  32655  funcnvmpt  32685  curry2ima  32720  intimafv  32722  cnvoprabOLD  32734  elicoelioo  32783  fzo0opth  32810  wrdt2ind  32920  swrdrn3  32922  orngsqr  33299  qusker  33342  dvdsrspss  33380  lsmsnorb  33384  1arithufdlem4  33540  r1pid2OLD  33594  algextdeglem8  33715  zarcls  33820  xrmulc1cn  33876  xrge0iifcnv  33879  ind1a  33983  esumfsup  34034  esumpcvgval  34042  esumcvg  34050  esum2dlem  34056  issgon  34087  eulerpartgbij  34337  eulerpartlemgh  34343  ballotlemsima  34480  bnj1366  34805  bnj553  34874  bnj964  34919  cusgredgex  35089  revwlk  35092  loop1cycl  35105  subfacp1lem3  35150  subfacp1lem5  35152  erdszelem9  35167  prv1n  35399  ply1divalg3  35610  quad3  35638  br6  35719  elintfv  35728  dfon2lem5  35751  dfon2lem8  35754  brbigcup  35862  dfbigcup2  35863  elfix  35867  ellimits  35874  snelsingles  35886  dfiota3  35887  imageval  35894  brapply  35902  brsuccf  35905  funpartlem  35906  brfullfun  35912  dfrecs2  35914  dfrdg4  35915  altopthbg  35932  altopthc  35935  altopthd  35936  altopelaltxp  35940  brsegle  36072  outsideofrflx  36091  elicc3  36283  nn0prpw  36289  opnregcld  36296  cldregopn  36297  fneval  36318  topfneec  36321  knoppndvlem9  36486  bj-elgab  36905  bj-gabima  36906  bj-elsngl  36934  bj-snglc  36935  bj-projval  36962  bj-disj2r  36994  bj-restreg  37065  bj-0int  37067  copsex2b  37106  bj-inftyexpitaudisj  37171  bj-inftyexpidisj  37176  bj-bary1lem1  37277  topdifinffinlem  37313  topdifinfeq  37316  fvineqsnf1  37376  curf  37558  uncf  37559  curunc  37562  unccur  37563  poimirlem2  37582  poimirlem16  37596  poimirlem17  37597  poimirlem19  37599  poimirlem20  37600  poimirlem27  37607  mblfinlem2  37618  mbfresfi  37626  itg2addnclem2  37632  ftc1anclem3  37655  fdc  37705  heibor1  37770  opidonOLD  37812  0rngo  37987  smprngopr  38012  isfldidl  38028  isfldidl2  38029  eqbrb  38188  eqelb  38190  ideq2  38263  relcnveq  38278  n0elqs  38282  disjressuc2  38344  elrelscnveq  38448  disjdmqscossss  38759  lcvnbtwn3  38984  lcvexchlem1  38990  lsatnem0  39001  opcon1b  39154  omllaw2N  39200  cmtbr2N  39209  leatb  39248  cvlsupr2  39299  glbconxN  39335  islln3  39467  llnexatN  39478  islpln3  39490  lplnexatN  39520  islvol3  39533  dalem-cly  39628  isline4N  39734  2llnma3r  39745  poml4N  39910  4atex2  40034  4atex2-0bOLDN  40036  cdlemefrs29bpre0  40353  cdlemftr3  40522  cdlemb3  40563  cdlemg17h  40625  cdlemg17pq  40629  cdlemg19  40641  cdlemg21  40643  tendoex  40932  dva1dim  40942  dihglb2  41299  doch11  41330  dochsordN  41331  lcfrlem9  41507  hlhillcs  41919  lcmineqlem4  41989  aks6d1c7lem2  42138  aks5lem3a  42146  aks5lem6  42149  unitscyglem2  42153  unitscyglem3  42154  metakunt1  42162  metakunt6  42167  metakunt15  42176  metakunt16  42177  addsubeq4com  42269  ef11d  42327  fimgmcyclem  42488  fsuppind  42545  elrfirn  42651  isnacs2  42662  isnacs3  42666  fiphp3d  42775  wopprc  42987  islnm2  43035  kercvrlsm  43040  fgraphopab  43164  tfsconcatlem  43298  tfsconcatrn  43304  tfsconcat0i  43307  tfsconcat0b  43308  tfsconcatrev  43310  oaun3lem1  43336  oadif1lem  43341  oadif1  43342  rp-fakeuninass  43478  snen1g  43486  iscard4  43495  sqrtcval  43603  frege124d  43723  frege129d  43725  frege92  43917  dffrege99  43924  clsk3nimkb  44002  clsk1indlem4  44006  clsk1indlem1  44007  ntrclsiso  44029  ntrclsk3  44032  ntrclsk13  44033  ntrneik4w  44062  extoimad  44126  int-sqdefd  44143  int-sqgeq0d  44148  radcnvrat  44283  bcc0  44309  opelopab4  44522  eqsbc2VD  44811  fzisoeu  45215  iuneqfzuz  45250  supxrleubrnmptf  45366  rexanuz2nf  45408  fsummulc1f  45492  fsumiunss  45496  fmul01lt1lem2  45506  sumnnodd  45551  fnlimfvre2  45598  limsupreuz  45658  limsupvaluz2  45659  liminfvalxr  45704  icccncfext  45808  cncfiooicc  45815  cncfioobdlem  45817  dvmptmulf  45858  dvmptfprodlem  45865  volioc  45893  itgioocnicc  45898  fourierdlem12  46040  fourierdlem20  46048  fourierdlem25  46053  fourierdlem33  46061  fourierdlem42  46070  fourierdlem52  46079  fourierdlem54  46081  fourierdlem57  46084  fourierdlem58  46085  fourierdlem59  46086  fourierdlem63  46090  fourierdlem65  46092  fourierdlem68  46095  fourierdlem73  46100  fourierdlem74  46101  fourierdlem75  46102  fourierdlem80  46107  fourierdlem81  46108  rrndistlt  46211  sge0ltfirpmpt2  46347  sge0pnfmpt  46366  hoidmv1le  46515  hoidmvle  46521  vonioolem2  46602  smflimlem3  46694  euabsneu  46943  funressnfv  46958  aiotaval  47010  reuf1odnf  47022  reuf1od  47023  afvpcfv0  47061  dfafn5a  47075  afvelrnb  47078  afvelrnb0  47079  dfaimafn2  47081  dfatsnafv2  47167  dfatdmfcoafv2  47169  f1oresf1o2  47206  0nelsetpreimafv  47264  fargshiftfo  47316  sprsymrelf1  47370  reupr  47396  fmtnorec2lem  47416  fmtnoprmfac1  47439  fmtnoprmfac2  47441  sfprmdvdsmersenne  47477  lighneallem2  47480  dfeven2  47523  dfodd3  47524  odd2np1ALTV  47548  even3prm2  47593  fppr2odd  47605  nnsum3primesgbe  47666  nnsum3primesle9  47668  clnbgrsym  47710  dfvopnbgr2  47725  isuspgrim0  47756  isuspgrimlem  47758  dfgric2  47768  grtriprop  47792  uspgrlimlem3  47814  0nodd  47893  2nodd  47895  lmod0rng  47952  rngcinvALTV  47999  ringcinvALTV  48033  lcoel0  48157  lindslinindimp2lem4  48190  ldepspr  48202  lincresunit3  48210  nn0sumshdiglemB  48354  nn0sumshdiglem1  48355  rrx2pnedifcoorneorr  48451  eenglngeehlnmlem1  48471  eenglngeehlnmlem2  48472  rrx2linest  48476  rrx2linest2  48478  rrxsphere  48482  line2ylem  48485  line2x  48488  itscnhlc0xyqsol  48499  itschlc0xyqsol1  48500  itsclinecirc0b  48508  2itscp  48515  inlinecirc02plem  48520