Theorem eqcom 2770

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-9 2156  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2755

This theorem is used by:  eqcoms  2771  eqcomi  2772  neqcomd  2773  eqeq2d  2774  eqabcbw  2838  eqabcb  2904  necom  3012  nesym  3015  gencbvex  3510  clel5  3622  eqsbc2  3805  sspsstri  4036  dfss  4098  ssdifim  4221  disj4  4415  reuprg0  4663  preq1b  4804  invdisj  5092  disjprg  5102  dtruALT  5354  reusv3  5371  opthg2  5452  copsex2g  5469  copsex4g  5471  opcom  5477  opeqsng  5479  opeqpr  5481  snopeqop  5482  propeqop  5483  opthwiener  5491  vopelopabsb  5507  brab2d  5516  opthprc  5719  elxp3  5721  relop  5833  dmopab3  5906  rnopab3  5943  rncoeq  5968  restidsing  6051  somin1  6133  xpcan  6174  xpcan2  6175  dfrel4v  6188  dmsnn0  6215  reu3op  6302  reuop  6303  opreu2reurex  6304  ordtri2  6405  ordtri2or3  6472  suc11  6479  on0eqel  6495  snsn0non  6496  iota1  6525  iotan0  6536  iotan0OLD  6537  sniota  6538  mptfnf  6685  fresaunres1  6766  dffn5  6954  fvelrnb  6956  dfimafn2  6959  funimass4  6960  feqmptdf  6966  fnsnfv  6975  dmfco  6992  funcnvmpt  7006  fndmdif  7052  fneqeql  7056  rexrn  7098  ralrn  7099  elrnrexdmb  7101  dffo4  7114  fssrescdmd  7138  funopsn  7162  funopsnOLD  7163  ftpg  7171  fprb  7209  ralima  7253  fvclss  7255  dff13  7268  f1eqcocnv  7319  fnssintima  7382  riotaeqimp  7413  eusvobj2  7422  f1ocnvfv3  7425  oprabidw  7461  oprabid  7462  oprabv  7490  eloprabga  7539  ovelimab  7609  onmindif2  7831  br1steqg  8033  br2ndeqg  8034  reldm  8065  dfoprab3  8076  opiota  8081  f1o2ndf1  8146  soseq  8189  brtpos2  8263  tpossym  8289  mpocurryd  8300  rdglim2  8454  tz7.48lemOLD  8465  oaf1o  8585  omopthi  8684  erth2  8787  brecop  8845  erovlem  8848  ecopovsym  8854  eceqoveq  8857  curf  8904  uncf  8905  xpcomco  9100  omxpenlem  9111  mapen  9174  nneneq  9235  unxpdomlem3  9263  unfilem1  9311  mapfien  9413  supgtoreq  9476  wemapsolem  9557  suc11reg  9633  inf3lem2  9643  inf3lem6  9647  ttrcltr  9730  djulf1o  10006  djurf1o  10007  infenaleph  10183  isinfcard  10184  dfac5  10220  cfeq0  10347  cfsuc  10348  ssfin4  10401  fin23lem25  10415  fin23lem22  10418  fin23lem40  10442  fin1a2lem5  10495  axcclem  10548  brdom7disj  10623  brdom6disj  10624  inar1  10873  psslinpr  11129  ltexprlem4  11137  ltsrpr  11175  mulgt0sr  11203  elreal  11229  ltresr  11238  leloe  11409  eqlei2  11434  addsubeq4  11585  subcan2  11596  negcon1  11623  negcon2  11624  addid0  11748  addeq0  11752  divmul2  11991  conjmul  12047  rereccl  12048  creur  12327  creui  12328  ind1a  12344  nndiv  12397  nn0sub  12669  elnn0z  12719  elznn0  12721  xrleloe  13286  ngtmnft  13309  icoshftf1o  13618  iccf1o  13640  fzen  13687  fzneuz  13755  injresinj  13939  fleqceilz  14007  mod0  14029  modmuladdnn0  14071  modirr  14098  addmodlteq  14102  nn0ennn  14135  hashrabsn01  14530  hashsdom  14538  hashgt12el2  14581  hashbclem  14610  hashfacen  14612  hashf1lem1  14613  hashtpg  14643  tpf1o  14659  fi1uzind  14665  ccatw2s1p1  14798  swrdrn3  14816  wrd2ind  14886  cshw1  14987  cshwsexa  14989  scshwfzeqfzo  14991  s2f1o  15082  wwlktovfo  15126  dmtrclfv  15186  cjreb  15305  leabs  15481  reusq0  15647  incexc2  16022  rpnnen2lem12  16408  dvdsval2  16440  dvdsabseq  16498  dvdsflip  16502  odd2np1  16526  oddm1even  16528  sqoddm1div8z  16539  m1exp1  16561  divalglem4  16581  divalglem8  16585  divalgb  16589  modremain  16593  zeqzmulgcd  16697  dfgcd2  16734  lcmfpr  16817  lcmftp  16826  lcmfunsnlem2  16830  divgcdcoprm0  16855  prm2orodd  16881  hashdvds  16967  oddprmdvds  17096  vdwlem12  17185  cshwshashlem1  17288  cshwsiun  17292  initoid  18191  termoid  18192  setcinv  18280  yonedainv  18470  joinfval  18560  joinfval2  18561  meetfval  18574  meetfval2  18575  latnle  18662  chnfi  18823  mgmidpfod  18872  sgrp2nmndlem3  19139  grpid  19201  grpinvcnv  19232  grplmulf1o  19238  grpraddf1o  19239  grpsubeq0  19251  grpsubadd  19253  grplactcnv  19268  ressmulgnnd  19303  isnsg4  19392  eqg0el  19413  cycsubmel  19430  conjghm  19478  conjnmzb  19482  gacan  19534  gapm  19535  cntzrec  19565  oppgcntz  19593  fvcosymgeq  19658  odmulgeq  19786  dfod2  19793  sylow3lem3  19858  sylow3lem6  19861  lssnle  19903  lsmhash  19934  efgredlemb  19975  efgrelexlemb  19979  dprd2d2  20275  ablfac1eulem  20303  pgpfac1lem2  20306  pgpfac1lem4  20309  dvdsrval  20606  dvdsr02  20617  01eq0ring  20796  0ring01eqbi2  20798  0ring01eqbi  20799  rngcinv  20904  ringcinv  20938  orngsqr  21138  rmodislmodlem  21219  lvecinv  21406  isfieldidl2  21556  rngqiprngimf1lem  21605  rspsn  21672  prmirredlem  21793  zndvds  21870  znleval  21875  psrbagconf1o  22252  mplmonmul  22360  gsummoncoe1  22641  evl1maprhm  22712  mat1dimelbas  22801  mat1dimbas  22802  1mavmul  22878  ma1repveval  22901  mulmarep1gsum1  22903  mdetunilem9  22950  m2cpminvid2lem  23087  pmatcollpw3lem  23116  mp2pm2mplem4  23142  toponsspwpw  23255  dmtopon  23256  cmpfi  23741  ssref  23846  qtopeu  24050  hmeoimaf1o  24104  txhmeo  24137  fbasrn  24218  rnelfmlem  24286  hauspwpwf1  24321  alexsubALTlem4  24384  qustgpopn  24454  qustgphaus  24457  fmucndlem  24624  isngp3  24932  isngp4  24946  metnrmlem1a  25193  icopnfcnv  25278  iccpnfcnv  25280  ivthle  25792  ivthle2  25793  dyadmbl  25936  mbfinf  26001  i1fmulclem  26038  itg1mulc  26040  mvth  26327  dvivth  26345  lhop2  26350  r1pid2  26495  dvdsq1p  26496  plyconz  26646  reeff1o  26789  coseq1  26868  recosf1o  26878  resinf1o  26879  efopn  27001  cxpeq  27100  logreclem  27105  affineequiv  27166  affineequiv4  27169  affineequivne  27170  quad2  27182  dcubic  27189  mcubic  27190  quart  27204  atandm2  27220  rlimcnp2  27309  amgm  27333  wilthlem2  27411  mumullem2  27522  sqff1o  27524  dvdsflf1o  27529  gausslemma2dlem0i  27706  lgseisenlem2  27718  lgsquadlem2  27723  2lgslem1c  27735  2lgsoddprmlem2  27751  2lgsoddprm  27758  2sq2  27775  addsq2reu  27782  2sqreultlem  27789  2sqreunnltlem  27792  2sqreulem3  27795  ltsval2  28028  ltsintdifex  28033  ltsres  28034  nosepon  28037  noextenddif  28040  nosepssdm  28058  nogt01o  28068  nosupprefixmo  28072  noinfprefixmo  28073  nosupno  28075  noinfno  28090  lesloe  28126  eqcuts2  28187  cutbdaylt  28199  elold  28260  made0  28264  lrrecfr  28344  subadds  28471  oncutlt  28665  z12sge0  28884  renegscl  28899  tgjustf  28950  legtrid  29069  legso  29077  islmib  29307  lmicom  29308  lmiinv  29312  lmimid  29314  lmiopp  29323  prlngsym  29434  colinearalglem2  29500  colinearalg  29503  ax5seglem4  29525  ax5seglem5  29526  axlowdimlem13  29547  axeuclidlem  29555  axeuclid  29556  axcontlem2  29558  axcontlem4  29560  elntg2  29578  structiedg0val  29615  uspgredgiedg  29771  uspgriedgedg  29772  usgredgsscusgredg  30055  fusgrn0degnn0  30095  umgr2v2evtxel  30118  vdiscusgrb  30126  uspgr2wlkeq  30241  wlk0prc  30248  wlklenvclwlk  30249  wlkp1lem8  30274  revwlk  30282  spthdep  30335  usgr2pthlem  30364  usgr2pth  30365  wlkiswwlksupgr2  30481  wlklnwwlkln2lem  30486  wwlksnextproplem3  30515  umgr2adedgwlk  30549  umgr2adedgspth  30552  umgr2wlkon  30554  usgrwwlks2on  30562  umgrwwlks2on  30563  elwwlks2  30573  elwspths2spth  30574  clwlkclwwlklem2a4  30603  clwlkclwwlklem2  30606  erclwwlkref  30626  clwwlkf  30653  erclwwlknref  30675  erclwwlknsym  30676  erclwwlkntr  30677  hashecclwwlkn1  30683  umgrhashecclwwlk  30684  loop1cycl  30759  eupth2lem2  30835  eucrct2eupth  30861  numclwwlkqhash  30991  isgrpo  31114  hvsubaddi  31683  hire  31711  shmodsi  32006  omlsilem  32019  chcon1i  32082  chnlei  32102  pjoml3i  32203  cmbr2i  32213  chscllem2  32255  adjsym  32450  eigorthi  32454  dfadj2  32502  adjval2  32508  cnvadj  32509  dmadjrnb  32523  adjvalval  32554  cnlnadjeui  32694  cnlnssadj  32697  adjbdln  32700  pjimai  32793  pjin2i  32810  pjin3i  32811  stadd3i  32865  largei  32884  cvnbtwn3  32905  cvnbtwn4  32906  mddmd2  32926  superpos  32971  atnemeq0  32994  sumdmdii  33032  sumdmdlem  33035  addltmulALT  33105  opreu2reuALT  33130  foresf1o  33157  difeq  33171  disjrdx  33242  fcoinvbr  33256  fmptco1f1o  33284  dfimafnf  33287  curry2ima  33359  intimafv  33361  receqid  33392  elicoelioo  33426  fzo0opth  33451  wrdt2ind  33572  gsummptp1  33674  gsummulsubdishift1  33685  cntrval2  33788  domnprodeq0  33896  qusker  33966  dvdsrspss  33998  lsmsnorb  34002  1arithufdlem4  34135  selvply1rhmlemb  34207  psrmonmul  34238  esplyind  34263  algextdeglem8  34412  zarcls  34562  xrmulc1cn  34618  xrge0iifcnv  34621  esumfsup  34758  esumpcvgval  34766  esumcvg  34774  esum2dlem  34780  issgon  34811  eulerpartgbij  35060  eulerpartlemgh  35066  ballotlemsima  35204  bnj1366  35515  bnj553  35584  bnj964  35629  dfscott3  35809  fineqvnttrclse  35866  maxssj0  35963  jf1o  35968  dfk12  35969  dfk22  35970  dfk32  35971  cusgredgex  36020  subfacp1lem3  36071  subfacp1lem5  36073  erdszelem9  36088  prv1n  36320  ply1divalg3  36531  quad3  36559  br6  36655  elintfv  36663  dfon2lem5  36682  dfon2lem8  36685  brbigcup  36793  dfbigcup2  36794  elfix  36798  ellimits  36805  snelsingles  36817  dfiota3  36818  imageval  36825  brapply  36833  lemsuccf  36836  dfsuccf2  36838  funpartlem  36839  brfullfun  36845  dfrecs2  36847  dfrdg4  36848  altopthbg  36866  altopthc  36869  altopthd  36870  altopelaltxp  36874  brsegle  37006  outsideofrflx  37025  elicc3  37238  nn0prpw  37244  opnregcld  37251  cldregopn  37252  fneval  37273  topfneec  37276  knoppndvlem9  37519  bj-elgab  37985  bj-gabima  37986  bj-elsngl  38014  bj-snglc  38015  bj-projval  38042  bj-disj2r  38074  bj-restreg  38165  bj-0int  38167  copsex2gd  38205  copsex2b  38207  bj-inftyexpitaudisj  38272  bj-inftyexpidisj  38277  bj-bary1lem1  38378  topdifinffinlem  38416  topdifinfeq  38419  fvineqsnf1  38479  curunc  38671  unccur  38672  poimirlem2  38686  poimirlem16  38700  poimirlem17  38701  poimirlem19  38703  poimirlem20  38704  poimirlem27  38711  mblfinlem2  38722  mbfresfi  38730  itg2addnclem2  38736  ftc1anclem3  38759  findcard4  38778  fdc  38825  heibor1  38890  opidonOLD  38932  0rngo  39107  smprngopr  39132  isfldidl  39148  isfldidl2  39149  eqbrb  39317  eqelb  39319  ideq2  39391  relcnveq  39406  n0elqs  39410  disjressuc2  39489  dfsucmap3  39541  dfsucmap4  39543  dmsucmap  39546  preuniqval  39574  elrelscnveq  39706  qseq  39811  disjdmqscossss  39984  lcvnbtwn3  40231  lcvexchlem1  40237  lsatnem0  40248  opcon1b  40401  omllaw2N  40447  cmtbr2N  40456  leatb  40495  cvlsupr2  40546  glbconxN  40581  islln3  40713  llnexatN  40724  islpln3  40736  lplnexatN  40766  islvol3  40779  dalem-cly  40874  isline4N  40980  2llnma3r  40991  poml4N  41156  4atex2  41280  4atex2-0bOLDN  41282  cdlemefrs29bpre0  41599  cdlemftr3  41768  cdlemb3  41809  cdlemg17h  41871  cdlemg17pq  41875  cdlemg19  41887  cdlemg21  41889  tendoex  42178  dva1dim  42188  dihglb2  42545  doch11  42576  dochsordN  42577  lcfrlem9  42753  hlhillcs  43161  lcmineqlem4  43228  aks6d1c7lem2  43377  aks5lem3a  43385  aks5lem6  43388  unitscyglem2  43392  unitscyglem3  43393  addsubeq4com  43483  ef11d  43536  redivmul2d  43643  fimgmcyclem  43743  fsuppind  43764  elrfirn  43852  isnacs2  43863  isnacs3  43867  fiphp3d  43972  wopprc  44183  islnm2  44226  kercvrlsm  44231  fgraphopab  44351  tfsconcatlem  44484  tfsconcatrn  44490  tfsconcat0i  44493  tfsconcat0b  44494  tfsconcatrev  44496  oaun3lem1  44522  oadif1lem  44527  oadif1  44528  rp-fakeuninass  44663  snen1g  44671  iscard4  44680  sqrtcval  44787  frege124d  44907  frege129d  44909  frege92  45101  dffrege99  45108  clsk3nimkb  45186  clsk1indlem4  45190  clsk1indlem1  45191  ntrclsiso  45213  ntrclsk3  45216  ntrclsk13  45217  ntrneik4w  45246  extoimad  45310  int-sqdefd  45327  int-sqgeq0d  45332  radcnvrat  45444  bcc0  45470  opelopab4  45679  eqsbc2VD  45967  fzisoeu  46461  iuneqfzuz  46492  supxrleubrnmptf  46606  rexanuz2nf  46647  fsummulc1f  46728  fsumiunss  46732  fmul01lt1lem2  46742  sumnnodd  46787  fnlimfvre2  46832  limsupreuz  46892  limsupvaluz2  46893  liminfvalxr  46938  icccncfext  47042  cncfiooicc  47049  cncfioobdlem  47051  dvmptmulf  47092  dvmptfprodlem  47099  volioc  47127  itgioocnicc  47132  fourierdlem12  47274  fourierdlem20  47282  fourierdlem25  47287  fourierdlem33  47295  fourierdlem42  47304  fourierdlem52  47313  fourierdlem54  47315  fourierdlem57  47318  fourierdlem58  47319  fourierdlem59  47320  fourierdlem63  47324  fourierdlem65  47326  fourierdlem68  47329  fourierdlem73  47334  fourierdlem74  47335  fourierdlem75  47336  fourierdlem80  47341  fourierdlem81  47342  rrndistlt  47445  sge0ltfirpmpt2  47581  sge0pnfmpt  47600  hoidmv1le  47749  hoidmvle  47755  vonioolem2  47836  smflimlem3  47928  chnsubseqwl  48034  cos5teq  48071  lambert0  48082  lamberte  48083  euabsneu  48243  funressnfv  48258  aiotaval  48310  aiotaexim  48313  reuf1odnf  48323  reuf1od  48324  afvpcfv0  48361  dfafn5a  48375  afvelrnb  48378  afvelrnb0  48379  dfaimafn2  48381  dfatsnafv2  48467  dfatdmfcoafv2  48469  f1oresf1o2  48506  ceilbi  48552  minusmodnep2tmod  48574  0nelsetpreimafv  48617  fargshiftfo  48669  sprsymrelf1  48723  reupr  48749  nprmmul1  48754  fmtnorec2lem  48772  fmtnoprmfac1  48795  fmtnoprmfac2  48797  sfprmdvdsmersenne  48833  lighneallem2  48836  dfeven2  48892  dfodd3  48893  odd2np1ALTV  48917  even3prm2  48962  fppr2odd  48974  nnsum3primesgbe  49035  nnsum3primesle9  49037  clnbgrsym  49081  dfvopnbgr2  49096  isuspgrim0  49137  isuspgrimlem  49138  dfgric2  49158  grtriprop  49184  uspgrlimlem3  49233  gpgvtxedg1  49307  pgnbgreunbgrlem2lem1  49357  pgnbgreunbgrlem2lem2  49358  0nodd  49412  2nodd  49414  lmod0rng  49471  rngcinvALTV  49518  ringcinvALTV  49552  isidom3  49587  lcoel0  49685  lindslinindimp2lem4  49718  ldepspr  49730  lincresunit3  49738  nn0sumshdiglemB  49877  nn0sumshdiglem1  49878  rrx2pnedifcoorneorr  49975  rrx2xpref1o  49976  eenglngeehlnmlem1  49995  eenglngeehlnmlem2  49996  rrx2linest  49999  rrx2linest2  50001  rrxsphere  50005  line2ylem  50008  line2x  50011  itscnhlc0xyqsol  50022  itschlc0xyqsol1  50023  itsclinecirc0b  50031  2itscp  50038  inlinecirc02plem  50043  brab2dd  50084  uptr2  50482