Theorem eqcom 2772

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

This proof depends on syntax axioms:   ↔ wb 209   = wceq 1570

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2757

This theorem is used by:  eqcoms  2773  eqcomi  2774  neqcomd  2775  eqeq2d  2776  eqabcbw  2839  eqabcb  2905  necom  3013  nesym  3016  gencbvex  3513  clel5  3626  eqsbc2  3809  dfss  3925  sspsstri  4061  ssdifim  4226  disj4  4419  reuprg0  4670  preq1b  4813  invdisj  5097  disjprg  5107  dtruALT  5361  reusv3  5378  opthg2  5463  copsex2g  5478  copsex4g  5480  opcom  5486  opeqsng  5488  opeqpr  5490  snopeqop  5491  propeqop  5492  opthwiener  5499  vopelopabsb  5515  brab2d  5524  opthprc  5727  elxp3  5729  relop  5838  dmopab3  5911  rnopab3  5948  rncoeq  5973  restidsing  6057  somin1  6135  xpcan  6176  xpcan2  6177  dfrel4v  6190  dmsnn0  6210  reu3op  6297  reuop  6298  opreu2reurex  6299  ordtri2  6400  ordtri2or3  6467  suc11  6474  on0eqel  6490  snsn0non  6491  iota1  6519  iotan0  6530  sniota  6531  mptfnf  6674  fresaunres1  6755  dffn5  6943  fvelrnb  6945  dfimafn2  6948  funimass4  6949  feqmptdf  6955  fnsnfv  6964  dmfco  6981  funcnvmpt  6995  fndmdif  7041  fneqeql  7045  rexrn  7086  ralrn  7087  elrnrexdmb  7089  dffo4  7102  fssrescdmd  7126  funopsn  7150  funopsnOLD  7151  ftpg  7159  fprb  7198  ralima  7242  fvclss  7244  dff13  7257  f1eqcocnv  7308  fnssintima  7371  riotaeqimp  7402  eusvobj2  7411  f1ocnvfv3  7414  oprabidw  7450  oprabid  7451  oprabv  7479  eloprabga  7528  ovelimab  7598  onmindif2  7812  br1steqg  8014  br2ndeqg  8015  dfoprab3  8057  opiota  8062  f1o2ndf1  8123  soseq  8161  brtpos2  8234  tpossym  8260  mpocurryd  8271  rdglim2  8425  tz7.48lem  8434  oaf1o  8554  omopthi  8653  erth2  8756  brecop  8814  erovlem  8817  ecopovsym  8823  eceqoveq  8826  xpcomco  9062  omxpenlem  9073  mapen  9136  nneneq  9197  unxpdomlem3  9225  unfilem1  9272  mapfien  9375  supgtoreq  9438  wemapsolem  9519  suc11reg  9595  inf3lem2  9605  inf3lem6  9609  ttrcltr  9692  djulf1o  9914  djurf1o  9915  infenaleph  10091  isinfcard  10092  dfac5  10128  cfeq0  10255  cfsuc  10256  ssfin4  10309  fin23lem25  10323  fin23lem22  10326  fin23lem40  10350  fin1a2lem5  10403  axcclem  10456  brdom7disj  10531  brdom6disj  10532  inar1  10779  psslinpr  11035  ltexprlem4  11043  ltsrpr  11081  mulgt0sr  11109  elreal  11135  ltresr  11144  leloe  11315  eqlei2  11340  addsubeq4  11491  subcan2  11502  negcon1  11529  negcon2  11530  addid0  11652  addeq0  11656  divmul2  11895  conjmul  11951  rereccl  11952  creur  12231  creui  12232  ind1a  12248  nndiv  12301  nn0sub  12573  elnn0z  12623  elznn0  12625  xrleloe  13189  ngtmnft  13212  icoshftf1o  13521  iccf1o  13543  fzen  13589  fzneuz  13657  injresinj  13841  fleqceilz  13909  mod0  13931  modmuladdnn0  13973  modirr  14000  addmodlteq  14004  nn0ennn  14037  hashrabsn01  14431  hashsdom  14439  hashgt12el2  14482  hashbclem  14511  hashfacen  14513  hashf1lem1  14514  hashtpg  14544  tpf1o  14560  fi1uzind  14566  ccatw2s1p1  14698  swrdrn3  14716  wrd2ind  14786  cshw1  14887  cshwsexa  14889  scshwfzeqfzo  14891  s2f1o  14981  wwlktovfo  15023  dmtrclfv  15083  cjreb  15202  leabs  15378  reusq0  15544  incexc2  15919  rpnnen2lem12  16307  dvdsval2  16339  dvdsabseq  16397  dvdsflip  16401  odd2np1  16425  oddm1even  16427  sqoddm1div8z  16438  m1exp1  16460  divalglem4  16480  divalglem8  16484  divalgb  16488  modremain  16492  zeqzmulgcd  16594  dfgcd2  16630  lcmfpr  16711  lcmftp  16720  lcmfunsnlem2  16724  divgcdcoprm0  16749  prm2orodd  16775  hashdvds  16860  oddprmdvds  16989  vdwlem12  17078  cshwshashlem1  17181  cshwsiun  17185  initoid  18084  termoid  18085  setcinv  18173  yonedainv  18363  joinfval  18453  joinfval2  18454  meetfval  18467  meetfval2  18468  latnle  18555  chnfi  18716  mgmidpfod  18764  sgrp2nmndlem3  19028  grpid  19090  grpinvcnv  19121  grplmulf1o  19127  grpraddf1o  19128  grpsubeq0  19140  grpsubadd  19142  grplactcnv  19157  ressmulgnnd  19192  isnsg4  19281  eqg0el  19302  cycsubmel  19319  conjghm  19367  conjnmzb  19371  gacan  19423  gapm  19424  cntzrec  19454  oppgcntz  19482  fvcosymgeq  19547  odmulgeq  19675  dfod2  19682  sylow3lem3  19747  sylow3lem6  19750  lssnle  19792  lsmhash  19823  efgredlemb  19864  efgrelexlemb  19868  dprd2d2  20164  ablfac1eulem  20192  pgpfac1lem2  20195  pgpfac1lem4  20198  dvdsrval  20493  dvdsr02  20504  01eq0ring  20682  0ring01eqbi2  20684  0ring01eqbi  20685  rngcinv  20790  ringcinv  20824  orngsqr  21023  rmodislmodlem  21104  lvecinv  21291  isfieldidl2  21441  rngqiprngimf1lem  21488  rspsn  21555  prmirredlem  21676  zndvds  21753  znleval  21758  psrbagconf1o  22133  mplmonmul  22241  gsummoncoe1  22522  evl1maprhm  22593  mat1dimelbas  22682  mat1dimbas  22683  1mavmul  22759  ma1repveval  22782  mulmarep1gsum1  22784  mdetunilem9  22831  m2cpminvid2lem  22965  pmatcollpw3lem  22994  mp2pm2mplem4  23020  toponsspwpw  23133  dmtopon  23134  cmpfi  23619  ssref  23724  qtopeu  23928  hmeoimaf1o  23982  txhmeo  24015  fbasrn  24096  rnelfmlem  24164  hauspwpwf1  24199  alexsubALTlem4  24262  qustgpopn  24332  qustgphaus  24335  fmucndlem  24502  isngp3  24810  isngp4  24824  metnrmlem1a  25071  icopnfcnv  25156  iccpnfcnv  25158  ivthle  25670  ivthle2  25671  dyadmbl  25814  mbfinf  25879  i1fmulclem  25916  itg1mulc  25918  mvth  26206  dvivth  26224  lhop2  26229  r1pid2  26374  dvdsq1p  26375  reeff1o  26665  coseq1  26745  recosf1o  26755  resinf1o  26756  efopn  26878  cxpeq  26977  logreclem  26982  affineequiv  27043  affineequiv4  27046  affineequivne  27047  quad2  27059  dcubic  27066  mcubic  27067  quart  27081  atandm2  27097  rlimcnp2  27186  amgm  27210  wilthlem2  27288  mumullem2  27399  sqff1o  27401  dvdsflf1o  27406  gausslemma2dlem0i  27583  lgseisenlem2  27595  lgsquadlem2  27600  2lgslem1c  27612  2lgsoddprmlem2  27628  2lgsoddprm  27635  2sq2  27652  addsq2reu  27659  2sqreultlem  27666  2sqreunnltlem  27669  2sqreulem3  27672  ltsval2  27875  ltsintdifex  27880  ltsres  27881  nosepon  27884  noextenddif  27887  nosepssdm  27905  nogt01o  27915  nosupprefixmo  27919  noinfprefixmo  27920  nosupno  27922  noinfno  27937  lesloe  27973  eqcuts2  28034  cutbdaylt  28046  elold  28107  made0  28111  lrrecfr  28191  subadds  28318  oncutlt  28512  z12sge0  28731  renegscl  28746  tgjustf  28797  legtrid  28915  legso  28923  islmib  29151  lmicom  29152  lmiinv  29156  lmimid  29158  lmiopp  29167  prlngsym  29250  colinearalglem2  29316  colinearalg  29319  ax5seglem4  29341  ax5seglem5  29342  axlowdimlem13  29363  axeuclidlem  29371  axeuclid  29372  axcontlem2  29374  axcontlem4  29376  elntg2  29394  structiedg0val  29431  uspgredgiedg  29587  uspgriedgedg  29588  usgredgsscusgredg  29871  fusgrn0degnn0  29911  umgr2v2evtxel  29934  vdiscusgrb  29942  uspgr2wlkeq  30057  wlk0prc  30064  wlklenvclwlk  30065  wlkp1lem8  30090  revwlk  30098  spthdep  30151  usgr2pthlem  30180  usgr2pth  30181  wlkiswwlksupgr2  30297  wlklnwwlkln2lem  30302  wwlksnextproplem3  30331  umgr2adedgwlk  30365  umgr2adedgspth  30368  umgr2wlkon  30370  usgrwwlks2on  30378  umgrwwlks2on  30379  elwwlks2  30389  elwspths2spth  30390  clwlkclwwlklem2a4  30419  clwlkclwwlklem2  30422  erclwwlkref  30442  clwwlkf  30469  erclwwlknref  30491  erclwwlknsym  30492  erclwwlkntr  30493  hashecclwwlkn1  30499  umgrhashecclwwlk  30500  loop1cycl  30575  eupth2lem2  30645  eucrct2eupth  30671  numclwwlkqhash  30801  isgrpo  30924  hvsubaddi  31493  hire  31521  shmodsi  31816  omlsilem  31829  chcon1i  31892  chnlei  31912  pjoml3i  32013  cmbr2i  32023  chscllem2  32065  adjsym  32260  eigorthi  32264  dfadj2  32312  adjval2  32318  cnvadj  32319  dmadjrnb  32333  adjvalval  32364  cnlnadjeui  32504  cnlnssadj  32507  adjbdln  32510  pjimai  32603  pjin2i  32620  pjin3i  32621  stadd3i  32675  largei  32694  cvnbtwn3  32715  cvnbtwn4  32716  mddmd2  32736  superpos  32781  atnemeq0  32804  sumdmdii  32842  sumdmdlem  32845  addltmulALT  32873  opreu2reuALT  32898  foresf1o  32925  difeq  32939  disjrdx  33011  fcoinvbr  33025  fmptco1f1o  33053  dfimafnf  33056  curry2ima  33129  intimafv  33131  receqid  33163  elicoelioo  33197  fzo0opth  33222  wrdt2ind  33343  gsummptp1  33445  gsummulsubdishift1  33456  cntrval2  33559  domnprodeq0  33667  qusker  33737  dvdsrspss  33768  lsmsnorb  33772  1arithufdlem4  33905  selvply1rhmlemb  33977  psrmonmul  34008  esplyind  34033  algextdeglem8  34182  zarcls  34332  xrmulc1cn  34388  xrge0iifcnv  34391  esumfsup  34528  esumpcvgval  34536  esumcvg  34544  esum2dlem  34550  issgon  34581  eulerpartgbij  34831  eulerpartlemgh  34837  ballotlemsima  34975  bnj1366  35286  bnj553  35355  bnj964  35400  dfscott3  35574  fineqvnttrclse  35598  cusgredgex  35668  subfacp1lem3  35715  subfacp1lem5  35717  erdszelem9  35732  prv1n  35964  ply1divalg3  36175  quad3  36203  br6  36290  elintfv  36298  dfon2lem5  36318  dfon2lem8  36321  brbigcup  36429  dfbigcup2  36430  elfix  36434  ellimits  36441  snelsingles  36453  dfiota3  36454  imageval  36461  brapply  36469  lemsuccf  36472  dfsuccf2  36474  funpartlem  36475  brfullfun  36481  dfrecs2  36483  dfrdg4  36484  altopthbg  36501  altopthc  36504  altopthd  36505  altopelaltxp  36509  brsegle  36641  outsideofrflx  36660  elicc3  36889  nn0prpw  36895  opnregcld  36902  cldregopn  36903  fneval  36924  topfneec  36927  knoppndvlem9  37170  bj-elgab  37636  bj-gabima  37637  bj-elsngl  37665  bj-snglc  37666  bj-projval  37693  bj-disj2r  37725  bj-restreg  37802  bj-0int  37804  copsex2gd  37843  copsex2b  37845  bj-inftyexpitaudisj  37910  bj-inftyexpidisj  37915  bj-bary1lem1  38016  topdifinffinlem  38054  topdifinfeq  38057  fvineqsnf1  38117  curf  38310  uncf  38311  curunc  38314  unccur  38315  poimirlem2  38334  poimirlem16  38348  poimirlem17  38349  poimirlem19  38351  poimirlem20  38352  poimirlem27  38359  mblfinlem2  38370  mbfresfi  38378  itg2addnclem2  38384  ftc1anclem3  38407  findcard4  38426  fdc  38458  heibor1  38523  opidonOLD  38565  0rngo  38740  smprngopr  38765  isfldidl  38781  isfldidl2  38782  eqbrb  38950  eqelb  38952  ideq2  39024  relcnveq  39039  n0elqs  39043  disjressuc2  39122  dfsucmap3  39174  dfsucmap4  39176  dmsucmap  39179  preuniqval  39207  elrelscnveq  39339  qseq  39444  disjdmqscossss  39617  lcvnbtwn3  39864  lcvexchlem1  39870  lsatnem0  39881  opcon1b  40034  omllaw2N  40080  cmtbr2N  40089  leatb  40128  cvlsupr2  40179  glbconxN  40214  islln3  40346  llnexatN  40357  islpln3  40369  lplnexatN  40399  islvol3  40412  dalem-cly  40507  isline4N  40613  2llnma3r  40624  poml4N  40789  4atex2  40913  4atex2-0bOLDN  40915  cdlemefrs29bpre0  41232  cdlemftr3  41401  cdlemb3  41442  cdlemg17h  41504  cdlemg17pq  41508  cdlemg19  41520  cdlemg21  41522  tendoex  41811  dva1dim  41821  dihglb2  42178  doch11  42209  dochsordN  42210  lcfrlem9  42386  hlhillcs  42794  lcmineqlem4  42861  aks6d1c7lem2  43010  aks5lem3a  43018  aks5lem6  43021  unitscyglem2  43025  unitscyglem3  43026  addsubeq4com  43118  ef11d  43177  redivmul2d  43284  fimgmcyclem  43378  fsuppind  43399  elrfirn  43503  isnacs2  43514  isnacs3  43518  fiphp3d  43623  wopprc  43834  islnm2  43882  kercvrlsm  43887  fgraphopab  44007  tfsconcatlem  44140  tfsconcatrn  44146  tfsconcat0i  44149  tfsconcat0b  44150  tfsconcatrev  44152  oaun3lem1  44178  oadif1lem  44183  oadif1  44184  rp-fakeuninass  44319  snen1g  44327  iscard4  44336  sqrtcval  44444  frege124d  44564  frege129d  44566  frege92  44758  dffrege99  44765  clsk3nimkb  44843  clsk1indlem4  44847  clsk1indlem1  44848  ntrclsiso  44870  ntrclsk3  44873  ntrclsk13  44874  ntrneik4w  44903  extoimad  44967  int-sqdefd  44984  int-sqgeq0d  44989  radcnvrat  45101  bcc0  45127  opelopab4  45337  eqsbc2VD  45625  fzisoeu  46096  iuneqfzuz  46128  supxrleubrnmptf  46242  rexanuz2nf  46283  fsummulc1f  46364  fsumiunss  46368  fmul01lt1lem2  46378  sumnnodd  46423  fnlimfvre2  46468  limsupreuz  46528  limsupvaluz2  46529  liminfvalxr  46574  icccncfext  46678  cncfiooicc  46685  cncfioobdlem  46687  dvmptmulf  46728  dvmptfprodlem  46735  volioc  46763  itgioocnicc  46768  fourierdlem12  46910  fourierdlem20  46918  fourierdlem25  46923  fourierdlem33  46931  fourierdlem42  46940  fourierdlem52  46949  fourierdlem54  46951  fourierdlem57  46954  fourierdlem58  46955  fourierdlem59  46956  fourierdlem63  46960  fourierdlem65  46962  fourierdlem68  46965  fourierdlem73  46970  fourierdlem74  46971  fourierdlem75  46972  fourierdlem80  46977  fourierdlem81  46978  rrndistlt  47081  sge0ltfirpmpt2  47217  sge0pnfmpt  47236  hoidmv1le  47385  hoidmvle  47391  vonioolem2  47472  smflimlem3  47564  chnsubseqwl  47672  cos5teq  47694  lambert0  47701  lamberte  47702  euabsneu  47842  funressnfv  47857  aiotaval  47909  reuf1odnf  47921  reuf1od  47922  afvpcfv0  47960  dfafn5a  47974  afvelrnb  47977  afvelrnb0  47978  dfaimafn2  47980  dfatsnafv2  48066  dfatdmfcoafv2  48068  f1oresf1o2  48105  ceilbi  48151  minusmodnep2tmod  48173  0nelsetpreimafv  48216  fargshiftfo  48268  sprsymrelf1  48322  reupr  48348  nprmmul1  48353  fmtnorec2lem  48371  fmtnoprmfac1  48394  fmtnoprmfac2  48396  sfprmdvdsmersenne  48432  lighneallem2  48435  dfeven2  48491  dfodd3  48492  odd2np1ALTV  48516  even3prm2  48561  fppr2odd  48573  nnsum3primesgbe  48634  nnsum3primesle9  48636  clnbgrsym  48680  dfvopnbgr2  48695  isuspgrim0  48736  isuspgrimlem  48737  dfgric2  48757  grtriprop  48783  uspgrlimlem3  48832  gpgvtxedg1  48906  pgnbgreunbgrlem2lem1  48956  pgnbgreunbgrlem2lem2  48957  0nodd  49011  2nodd  49013  lmod0rng  49070  rngcinvALTV  49117  ringcinvALTV  49151  isidom3  49186  lcoel0  49284  lindslinindimp2lem4  49317  ldepspr  49329  lincresunit3  49337  nn0sumshdiglemB  49476  nn0sumshdiglem1  49477  rrx2pnedifcoorneorr  49573  eenglngeehlnmlem1  49593  eenglngeehlnmlem2  49594  rrx2linest  49598  rrx2linest2  49600  rrxsphere  49604  line2ylem  49607  line2x  49610  itscnhlc0xyqsol  49621  itschlc0xyqsol1  49622  itsclinecirc0b  49630  2itscp  49637  inlinecirc02plem  49642  brab2dd  49682  uptr2  50075