Theorem eqcom 2767

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 2766	. 2 ⊢ (𝐴 = 𝐵 → 𝐵 = 𝐴)
3		id 23	. . 3 ⊢ (𝐵 = 𝐴 → 𝐵 = 𝐴)
4	3	eqcomd 2766	. 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 2155  ax-ext 2732

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

This theorem is used by:  eqcoms  2768  eqcomi  2769  neqcomd  2770  eqeq2d  2771  eqabcbw  2834  eqabcb  2900  necom  3008  nesym  3011  gencbvex  3506  clel5  3619  eqsbc2  3802  dfss  3918  sspsstri  4054  ssdifim  4219  disj4  4412  reuprg0  4663  preq1b  4806  invdisj  5089  disjprg  5099  dtruALT  5353  reusv3  5370  opthg2  5455  copsex2g  5470  copsex4g  5472  opcom  5478  opeqsng  5480  opeqpr  5482  snopeqop  5483  propeqop  5484  opthwiener  5491  vopelopabsb  5507  brab2d  5516  opthprc  5719  elxp3  5721  relop  5830  dmopab3  5903  rnopab3  5940  rncoeq  5965  restidsing  6049  somin1  6127  xpcan  6169  xpcan2  6170  dfrel4v  6183  dmsnn0  6203  reu3op  6290  reuop  6291  opreu2reurex  6292  ordtri2  6393  ordtri2or3  6460  suc11  6467  on0eqel  6483  snsn0non  6484  iota1  6512  iotan0  6523  sniota  6524  mptfnf  6668  fresaunres1  6749  dffn5  6937  fvelrnb  6939  dfimafn2  6942  funimass4  6943  feqmptdf  6949  fnsnfv  6958  dmfco  6975  funcnvmpt  6989  fndmdif  7035  fneqeql  7039  rexrn  7081  ralrn  7082  elrnrexdmb  7084  dffo4  7097  fssrescdmd  7121  funopsn  7145  funopsnOLD  7146  ftpg  7154  fprb  7193  ralima  7237  fvclss  7239  dff13  7252  f1eqcocnv  7303  fnssintima  7366  riotaeqimp  7397  eusvobj2  7406  f1ocnvfv3  7409  oprabidw  7445  oprabid  7446  oprabv  7474  eloprabga  7523  ovelimab  7593  onmindif2  7807  br1steqg  8009  br2ndeqg  8010  dfoprab3  8052  opiota  8057  f1o2ndf1  8120  soseq  8158  brtpos2  8231  tpossym  8257  mpocurryd  8268  rdglim2  8422  tz7.48lemOLD  8433  oaf1o  8553  omopthi  8652  erth2  8755  brecop  8813  erovlem  8816  ecopovsym  8822  eceqoveq  8825  curf  8872  uncf  8873  xpcomco  9068  omxpenlem  9079  mapen  9142  nneneq  9203  unxpdomlem3  9231  unfilem1  9278  mapfien  9381  supgtoreq  9444  wemapsolem  9525  suc11reg  9601  inf3lem2  9611  inf3lem6  9615  ttrcltr  9698  djulf1o  9920  djurf1o  9921  infenaleph  10097  isinfcard  10098  dfac5  10134  cfeq0  10261  cfsuc  10262  ssfin4  10315  fin23lem25  10329  fin23lem22  10332  fin23lem40  10356  fin1a2lem5  10409  axcclem  10462  brdom7disj  10537  brdom6disj  10538  inar1  10787  psslinpr  11043  ltexprlem4  11051  ltsrpr  11089  mulgt0sr  11117  elreal  11143  ltresr  11152  leloe  11323  eqlei2  11348  addsubeq4  11499  subcan2  11510  negcon1  11537  negcon2  11538  addid0  11660  addeq0  11664  divmul2  11903  conjmul  11959  rereccl  11960  creur  12239  creui  12240  ind1a  12256  nndiv  12309  nn0sub  12581  elnn0z  12631  elznn0  12633  xrleloe  13198  ngtmnft  13221  icoshftf1o  13530  iccf1o  13552  fzen  13598  fzneuz  13666  injresinj  13850  fleqceilz  13918  mod0  13940  modmuladdnn0  13982  modirr  14009  addmodlteq  14013  nn0ennn  14046  hashrabsn01  14440  hashsdom  14448  hashgt12el2  14491  hashbclem  14520  hashfacen  14522  hashf1lem1  14523  hashtpg  14553  tpf1o  14569  fi1uzind  14575  ccatw2s1p1  14707  swrdrn3  14725  wrd2ind  14795  cshw1  14896  cshwsexa  14898  scshwfzeqfzo  14900  s2f1o  14990  wwlktovfo  15034  dmtrclfv  15094  cjreb  15213  leabs  15389  reusq0  15555  incexc2  15930  rpnnen2lem12  16316  dvdsval2  16348  dvdsabseq  16406  dvdsflip  16410  odd2np1  16434  oddm1even  16436  sqoddm1div8z  16447  m1exp1  16469  divalglem4  16489  divalglem8  16493  divalgb  16497  modremain  16501  zeqzmulgcd  16603  dfgcd2  16639  lcmfpr  16720  lcmftp  16729  lcmfunsnlem2  16733  divgcdcoprm0  16758  prm2orodd  16784  hashdvds  16869  oddprmdvds  16998  vdwlem12  17087  cshwshashlem1  17190  cshwsiun  17194  initoid  18093  termoid  18094  setcinv  18182  yonedainv  18372  joinfval  18462  joinfval2  18463  meetfval  18476  meetfval2  18477  latnle  18564  chnfi  18725  mgmidpfod  18773  sgrp2nmndlem3  19040  grpid  19102  grpinvcnv  19133  grplmulf1o  19139  grpraddf1o  19140  grpsubeq0  19152  grpsubadd  19154  grplactcnv  19169  ressmulgnnd  19204  isnsg4  19293  eqg0el  19314  cycsubmel  19331  conjghm  19379  conjnmzb  19383  gacan  19435  gapm  19436  cntzrec  19466  oppgcntz  19494  fvcosymgeq  19559  odmulgeq  19687  dfod2  19694  sylow3lem3  19759  sylow3lem6  19762  lssnle  19804  lsmhash  19835  efgredlemb  19876  efgrelexlemb  19880  dprd2d2  20176  ablfac1eulem  20204  pgpfac1lem2  20207  pgpfac1lem4  20210  dvdsrval  20505  dvdsr02  20516  01eq0ring  20694  0ring01eqbi2  20696  0ring01eqbi  20697  rngcinv  20802  ringcinv  20836  orngsqr  21035  rmodislmodlem  21116  lvecinv  21303  isfieldidl2  21453  rngqiprngimf1lem  21500  rspsn  21567  prmirredlem  21688  zndvds  21765  znleval  21770  psrbagconf1o  22147  mplmonmul  22255  gsummoncoe1  22536  evl1maprhm  22607  mat1dimelbas  22696  mat1dimbas  22697  1mavmul  22773  ma1repveval  22796  mulmarep1gsum1  22798  mdetunilem9  22845  m2cpminvid2lem  22982  pmatcollpw3lem  23011  mp2pm2mplem4  23037  toponsspwpw  23150  dmtopon  23151  cmpfi  23636  ssref  23741  qtopeu  23945  hmeoimaf1o  23999  txhmeo  24032  fbasrn  24113  rnelfmlem  24181  hauspwpwf1  24216  alexsubALTlem4  24279  qustgpopn  24349  qustgphaus  24352  fmucndlem  24519  isngp3  24827  isngp4  24841  metnrmlem1a  25088  icopnfcnv  25173  iccpnfcnv  25175  ivthle  25687  ivthle2  25688  dyadmbl  25831  mbfinf  25896  i1fmulclem  25933  itg1mulc  25935  mvth  26222  dvivth  26240  lhop2  26245  r1pid2  26390  dvdsq1p  26391  plyconz  26543  reeff1o  26686  coseq1  26765  recosf1o  26775  resinf1o  26776  efopn  26898  cxpeq  26997  logreclem  27002  affineequiv  27063  affineequiv4  27066  affineequivne  27067  quad2  27079  dcubic  27086  mcubic  27087  quart  27101  atandm2  27117  rlimcnp2  27206  amgm  27230  wilthlem2  27308  mumullem2  27419  sqff1o  27421  dvdsflf1o  27426  gausslemma2dlem0i  27603  lgseisenlem2  27615  lgsquadlem2  27620  2lgslem1c  27632  2lgsoddprmlem2  27648  2lgsoddprm  27655  2sq2  27672  addsq2reu  27679  2sqreultlem  27686  2sqreunnltlem  27689  2sqreulem3  27692  ltsval2  27895  ltsintdifex  27900  ltsres  27901  nosepon  27904  noextenddif  27907  nosepssdm  27925  nogt01o  27935  nosupprefixmo  27939  noinfprefixmo  27940  nosupno  27942  noinfno  27957  lesloe  27993  eqcuts2  28054  cutbdaylt  28066  elold  28127  made0  28131  lrrecfr  28211  subadds  28338  oncutlt  28532  z12sge0  28751  renegscl  28766  tgjustf  28817  legtrid  28936  legso  28944  islmib  29174  lmicom  29175  lmiinv  29179  lmimid  29181  lmiopp  29190  prlngsym  29301  colinearalglem2  29367  colinearalg  29370  ax5seglem4  29392  ax5seglem5  29393  axlowdimlem13  29414  axeuclidlem  29422  axeuclid  29423  axcontlem2  29425  axcontlem4  29427  elntg2  29445  structiedg0val  29482  uspgredgiedg  29638  uspgriedgedg  29639  usgredgsscusgredg  29922  fusgrn0degnn0  29962  umgr2v2evtxel  29985  vdiscusgrb  29993  uspgr2wlkeq  30108  wlk0prc  30115  wlklenvclwlk  30116  wlkp1lem8  30141  revwlk  30149  spthdep  30202  usgr2pthlem  30231  usgr2pth  30232  wlkiswwlksupgr2  30348  wlklnwwlkln2lem  30353  wwlksnextproplem3  30382  umgr2adedgwlk  30416  umgr2adedgspth  30419  umgr2wlkon  30421  usgrwwlks2on  30429  umgrwwlks2on  30430  elwwlks2  30440  elwspths2spth  30441  clwlkclwwlklem2a4  30470  clwlkclwwlklem2  30473  erclwwlkref  30493  clwwlkf  30520  erclwwlknref  30542  erclwwlknsym  30543  erclwwlkntr  30544  hashecclwwlkn1  30550  umgrhashecclwwlk  30551  loop1cycl  30626  eupth2lem2  30702  eucrct2eupth  30728  numclwwlkqhash  30858  isgrpo  30981  hvsubaddi  31550  hire  31578  shmodsi  31873  omlsilem  31886  chcon1i  31949  chnlei  31969  pjoml3i  32070  cmbr2i  32080  chscllem2  32122  adjsym  32317  eigorthi  32321  dfadj2  32369  adjval2  32375  cnvadj  32376  dmadjrnb  32390  adjvalval  32421  cnlnadjeui  32561  cnlnssadj  32564  adjbdln  32567  pjimai  32660  pjin2i  32677  pjin3i  32678  stadd3i  32732  largei  32751  cvnbtwn3  32772  cvnbtwn4  32773  mddmd2  32793  superpos  32838  atnemeq0  32861  sumdmdii  32899  sumdmdlem  32902  addltmulALT  32930  opreu2reuALT  32955  foresf1o  32982  difeq  32996  disjrdx  33067  fcoinvbr  33081  fmptco1f1o  33109  dfimafnf  33112  curry2ima  33184  intimafv  33186  receqid  33218  elicoelioo  33252  fzo0opth  33277  wrdt2ind  33398  gsummptp1  33500  gsummulsubdishift1  33511  cntrval2  33614  domnprodeq0  33722  qusker  33792  dvdsrspss  33823  lsmsnorb  33827  1arithufdlem4  33960  selvply1rhmlemb  34032  psrmonmul  34063  esplyind  34088  algextdeglem8  34237  zarcls  34387  xrmulc1cn  34443  xrge0iifcnv  34446  esumfsup  34583  esumpcvgval  34591  esumcvg  34599  esum2dlem  34605  issgon  34636  eulerpartgbij  34886  eulerpartlemgh  34892  ballotlemsima  35030  bnj1366  35341  bnj553  35410  bnj964  35455  dfscott3  35629  fineqvnttrclse  35653  cusgredgex  35723  subfacp1lem3  35764  subfacp1lem5  35766  erdszelem9  35781  prv1n  36013  ply1divalg3  36224  quad3  36252  br6  36339  elintfv  36347  dfon2lem5  36367  dfon2lem8  36370  brbigcup  36478  dfbigcup2  36479  elfix  36483  ellimits  36490  snelsingles  36502  dfiota3  36503  imageval  36510  brapply  36518  lemsuccf  36521  dfsuccf2  36523  funpartlem  36524  brfullfun  36530  dfrecs2  36532  dfrdg4  36533  altopthbg  36551  altopthc  36554  altopthd  36555  altopelaltxp  36559  brsegle  36691  outsideofrflx  36710  elicc3  36939  nn0prpw  36945  opnregcld  36952  cldregopn  36953  fneval  36974  topfneec  36977  knoppndvlem9  37220  bj-elgab  37686  bj-gabima  37687  bj-elsngl  37715  bj-snglc  37716  bj-projval  37743  bj-disj2r  37775  bj-restreg  37852  bj-0int  37854  copsex2gd  37893  copsex2b  37895  bj-inftyexpitaudisj  37960  bj-inftyexpidisj  37965  bj-bary1lem1  38066  topdifinffinlem  38104  topdifinfeq  38107  fvineqsnf1  38167  curunc  38359  unccur  38360  poimirlem2  38374  poimirlem16  38388  poimirlem17  38389  poimirlem19  38391  poimirlem20  38392  poimirlem27  38399  mblfinlem2  38410  mbfresfi  38418  itg2addnclem2  38424  ftc1anclem3  38447  findcard4  38466  fdc  38498  heibor1  38563  opidonOLD  38605  0rngo  38780  smprngopr  38805  isfldidl  38821  isfldidl2  38822  eqbrb  38990  eqelb  38992  ideq2  39064  relcnveq  39079  n0elqs  39083  disjressuc2  39162  dfsucmap3  39214  dfsucmap4  39216  dmsucmap  39219  preuniqval  39247  elrelscnveq  39379  qseq  39484  disjdmqscossss  39657  lcvnbtwn3  39904  lcvexchlem1  39910  lsatnem0  39921  opcon1b  40074  omllaw2N  40120  cmtbr2N  40129  leatb  40168  cvlsupr2  40219  glbconxN  40254  islln3  40386  llnexatN  40397  islpln3  40409  lplnexatN  40439  islvol3  40452  dalem-cly  40547  isline4N  40653  2llnma3r  40664  poml4N  40829  4atex2  40953  4atex2-0bOLDN  40955  cdlemefrs29bpre0  41272  cdlemftr3  41441  cdlemb3  41482  cdlemg17h  41544  cdlemg17pq  41548  cdlemg19  41560  cdlemg21  41562  tendoex  41851  dva1dim  41861  dihglb2  42218  doch11  42249  dochsordN  42250  lcfrlem9  42426  hlhillcs  42834  lcmineqlem4  42901  aks6d1c7lem2  43050  aks5lem3a  43058  aks5lem6  43061  unitscyglem2  43065  unitscyglem3  43066  addsubeq4com  43158  ef11d  43217  redivmul2d  43324  fimgmcyclem  43418  fsuppind  43439  elrfirn  43543  isnacs2  43554  isnacs3  43558  fiphp3d  43663  wopprc  43874  islnm2  43922  kercvrlsm  43927  fgraphopab  44047  tfsconcatlem  44180  tfsconcatrn  44186  tfsconcat0i  44189  tfsconcat0b  44190  tfsconcatrev  44192  oaun3lem1  44218  oadif1lem  44223  oadif1  44224  rp-fakeuninass  44359  snen1g  44367  iscard4  44376  sqrtcval  44484  frege124d  44604  frege129d  44606  frege92  44798  dffrege99  44805  clsk3nimkb  44883  clsk1indlem4  44887  clsk1indlem1  44888  ntrclsiso  44910  ntrclsk3  44913  ntrclsk13  44914  ntrneik4w  44943  extoimad  45007  int-sqdefd  45024  int-sqgeq0d  45029  radcnvrat  45141  bcc0  45167  opelopab4  45377  eqsbc2VD  45665  fzisoeu  46136  iuneqfzuz  46168  supxrleubrnmptf  46282  rexanuz2nf  46323  fsummulc1f  46404  fsumiunss  46408  fmul01lt1lem2  46418  sumnnodd  46463  fnlimfvre2  46508  limsupreuz  46568  limsupvaluz2  46569  liminfvalxr  46614  icccncfext  46718  cncfiooicc  46725  cncfioobdlem  46727  dvmptmulf  46768  dvmptfprodlem  46775  volioc  46803  itgioocnicc  46808  fourierdlem12  46950  fourierdlem20  46958  fourierdlem25  46963  fourierdlem33  46971  fourierdlem42  46980  fourierdlem52  46989  fourierdlem54  46991  fourierdlem57  46994  fourierdlem58  46995  fourierdlem59  46996  fourierdlem63  47000  fourierdlem65  47002  fourierdlem68  47005  fourierdlem73  47010  fourierdlem74  47011  fourierdlem75  47012  fourierdlem80  47017  fourierdlem81  47018  rrndistlt  47121  sge0ltfirpmpt2  47257  sge0pnfmpt  47276  hoidmv1le  47425  hoidmvle  47431  vonioolem2  47512  smflimlem3  47604  chnsubseqwl  47710  cos5teq  47747  lambert0  47758  lamberte  47759  euabsneu  47919  funressnfv  47934  aiotaval  47986  reuf1odnf  47998  reuf1od  47999  afvpcfv0  48037  dfafn5a  48051  afvelrnb  48054  afvelrnb0  48055  dfaimafn2  48057  dfatsnafv2  48143  dfatdmfcoafv2  48145  f1oresf1o2  48182  ceilbi  48228  minusmodnep2tmod  48250  0nelsetpreimafv  48293  fargshiftfo  48345  sprsymrelf1  48399  reupr  48425  nprmmul1  48430  fmtnorec2lem  48448  fmtnoprmfac1  48471  fmtnoprmfac2  48473  sfprmdvdsmersenne  48509  lighneallem2  48512  dfeven2  48568  dfodd3  48569  odd2np1ALTV  48593  even3prm2  48638  fppr2odd  48650  nnsum3primesgbe  48711  nnsum3primesle9  48713  clnbgrsym  48757  dfvopnbgr2  48772  isuspgrim0  48813  isuspgrimlem  48814  dfgric2  48834  grtriprop  48860  uspgrlimlem3  48909  gpgvtxedg1  48983  pgnbgreunbgrlem2lem1  49033  pgnbgreunbgrlem2lem2  49034  0nodd  49088  2nodd  49090  lmod0rng  49147  rngcinvALTV  49194  ringcinvALTV  49228  isidom3  49263  lcoel0  49361  lindslinindimp2lem4  49394  ldepspr  49406  lincresunit3  49414  nn0sumshdiglemB  49553  nn0sumshdiglem1  49554  rrx2pnedifcoorneorr  49650  eenglngeehlnmlem1  49670  eenglngeehlnmlem2  49671  rrx2linest  49675  rrx2linest2  49677  rrxsphere  49681  line2ylem  49684  line2x  49687  itscnhlc0xyqsol  49698  itschlc0xyqsol1  49699  itsclinecirc0b  49707  2itscp  49714  inlinecirc02plem  49719  brab2dd  49759  uptr2  50150