Theorem eqcom 2741

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

Syntax hints:   ↔ wb 206   = wceq 1536

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-cleq 2726

This theorem is referenced by:  eqcoms  2742  eqcomi  2743  neqcomd  2744  eqeq2d  2745  eqtr2OLD  2759  eqtr3OLD  2761  eqabcb  2880  necom  2991  nesym  2994  pm13.181OLD  3021  gencbvex  3540  clel5  3664  eqsbc2  3859  dfss  3981  sspsstri  4114  ssnelpss  4123  ssdifim  4278  disj  4455  disj4  4464  reuprg0  4706  preq1b  4850  invdisj  5133  disjprg  5143  dtruALT  5393  reusv3  5410  opthg2  5489  copsex2g  5503  copsex4g  5504  opcom  5510  opeqsng  5512  opeqpr  5514  snopeqop  5515  propeqop  5516  opthwiener  5523  vopelopabsb  5538  opthprc  5752  elxp3  5754  relop  5863  dmopab3  5932  rnopab3  5969  rncoeq  5992  restidsing  6072  somin1  6155  xpcan  6197  xpcan2  6198  dfrel4v  6211  dmsnn0  6228  reu3op  6313  reuop  6314  opreu2reurex  6315  ordtri2  6420  ordtri2or3  6485  suc11  6492  on0eqel  6509  snsn0non  6510  iota1  6539  iotan0  6552  sniota  6553  mptfnf  6703  fresaunres1  6781  dffn5  6966  fvelrnb  6968  dfimafn2  6971  funimass4  6972  feqmptdf  6978  fnsnfv  6987  dmfco  7004  fndmdif  7061  fneqeql  7065  rexrn  7106  ralrn  7107  elrnrexdmb  7109  dffo4  7122  fssrescdmd  7145  funopsn  7167  ftpg  7175  fprb  7213  ralima  7256  reximaOLD  7258  ralimaOLD  7259  fvclss  7260  dff13  7274  f1eqcocnv  7320  fnssintima  7381  imaeqsexvOLD  7382  riotaeqimp  7413  eusvobj2  7422  f1ocnvfv3  7425  oprabidw  7461  oprabid  7462  oprabv  7492  eloprabga  7540  eloprabgaOLD  7541  ovelimab  7610  onmindif2  7826  br1steqg  8034  br2ndeqg  8035  dfoprab3  8077  opiota  8082  f1o2ndf1  8145  soseq  8182  brtpos2  8255  tpossym  8281  mpocurryd  8292  rdglim2  8470  tz7.48lem  8479  oaf1o  8599  omopthi  8697  erth2  8795  brecop  8848  erovlem  8851  ecopovsym  8857  eceqoveq  8860  xpcomco  9100  omxpenlem  9111  mapen  9179  nneneq  9243  nneneqOLD  9255  unxpdomlem3  9285  unfilem1  9340  mapfien  9445  supgtoreq  9507  wemapsolem  9587  suc11reg  9656  inf3lem2  9666  inf3lem6  9670  ttrcltr  9753  djulf1o  9949  djurf1o  9950  infenaleph  10128  isinfcard  10129  dfac5  10166  cfeq0  10293  cfsuc  10294  ssfin4  10347  fin23lem25  10361  fin23lem22  10364  fin23lem40  10388  fin1a2lem5  10441  axcclem  10494  brdom7disj  10568  brdom6disj  10569  inar1  10812  psslinpr  11068  ltexprlem4  11076  ltsrpr  11114  mulgt0sr  11142  elreal  11168  ltresr  11177  leloe  11344  eqlei2  11369  addsubeq4  11520  subcan2  11531  negcon1  11558  negcon2  11559  addid0  11679  addeq0  11683  divmul2  11923  conjmul  11981  rereccl  11982  creur  12257  creui  12258  nndiv  12309  nn0sub  12573  elnn0z  12623  elznn0  12625  xrleloe  13182  ngtmnft  13204  icoshftf1o  13510  iccf1o  13532  fzen  13577  fzneuz  13644  injresinj  13823  fleqceilz  13890  mod0  13912  modmuladdnn0  13952  modirr  13979  addmodlteq  13983  nn0ennn  14016  hashrabsn01  14408  hashsdom  14416  hashgt12el2  14458  hashbclem  14487  hashfacen  14489  hashf1lem1  14490  hashtpg  14520  tpf1o  14536  fi1uzind  14542  ccatw2s1p1  14670  wrd2ind  14757  cshw1  14856  cshwsexa  14858  scshwfzeqfzo  14861  s2f1o  14951  wwlktovfo  14993  dmtrclfv  15053  cjreb  15158  leabs  15334  reusq0  15497  incexc2  15870  rpnnen2lem12  16257  dvdsval2  16289  dvdsabseq  16346  dvdsflip  16350  odd2np1  16374  oddm1even  16376  sqoddm1div8z  16387  m1exp1  16409  divalglem4  16429  divalglem8  16433  divalgb  16437  modremain  16441  zeqzmulgcd  16543  dfgcd2  16579  lcmfpr  16660  lcmftp  16669  lcmfunsnlem2  16673  divgcdcoprm0  16698  prm2orodd  16724  hashdvds  16808  oddprmdvds  16936  vdwlem12  17025  cshwshashlem1  17129  cshwsiun  17133  initoid  18054  termoid  18055  setcinv  18143  yonedainv  18337  joinfval  18430  joinfval2  18431  meetfval  18444  meetfval2  18445  latnle  18530  sgrp2nmndlem3  18950  grpid  19005  grpinvcnv  19036  grplmulf1o  19043  grpraddf1o  19044  grpsubeq0  19056  grpsubadd  19058  grplactcnv  19073  ressmulgnnd  19108  isnsg4  19197  eqg0el  19213  cycsubmel  19230  conjghm  19279  conjnmzb  19283  gacan  19335  gapm  19336  cntzrec  19366  oppgcntz  19397  fvcosymgeq  19461  odmulgeq  19589  dfod2  19596  sylow3lem3  19661  sylow3lem6  19664  lssnle  19706  lsmhash  19737  efgredlemb  19778  efgrelexlemb  19782  dprd2d2  20078  ablfac1eulem  20106  pgpfac1lem2  20109  pgpfac1lem4  20112  dvdsrval  20377  dvdsr02  20388  01eq0ring  20546  0ring01eqbi  20548  rngcinv  20653  ringcinv  20687  rmodislmodlem  20943  lvecinv  21132  rngqiprngimf1lem  21321  rspsn  21360  dfcnfldOLD  21397  prmirredlem  21500  zndvds  21585  znleval  21590  psrbagconf1o  21966  mplmonmul  22071  gsummoncoe1  22327  evl1maprhm  22398  mat1dimelbas  22492  mat1dimbas  22493  1mavmul  22569  ma1repveval  22592  mulmarep1gsum1  22594  mdetunilem9  22641  m2cpminvid2lem  22775  pmatcollpw3lem  22804  mp2pm2mplem4  22830  toponsspwpw  22943  dmtopon  22944  cmpfi  23431  ssref  23535  qtopeu  23739  hmeoimaf1o  23793  txhmeo  23826  fbasrn  23907  rnelfmlem  23975  hauspwpwf1  24010  alexsubALTlem4  24073  qustgpopn  24143  qustgphaus  24146  fmucndlem  24315  isngp3  24626  isngp4  24640  metnrmlem1a  24893  icopnfcnv  24986  iccpnfcnv  24988  ivthle  25504  ivthle2  25505  dyadmbl  25648  mbfinf  25713  i1fmulclem  25751  itg1mulc  25753  mvth  26045  dvivth  26063  lhop2  26068  r1pid2  26215  dvdsq1p  26216  reeff1o  26505  coseq1  26581  recosf1o  26591  resinf1o  26592  efopn  26714  cxpeq  26814  logreclem  26819  affineequiv  26880  affineequiv4  26883  affineequivne  26884  quad2  26896  dcubic  26903  mcubic  26904  quart  26918  atandm2  26934  rlimcnp2  27023  amgm  27048  wilthlem2  27126  mumullem2  27237  sqff1o  27239  dvdsflf1o  27244  gausslemma2dlem0i  27422  lgseisenlem2  27434  lgsquadlem2  27439  2lgslem1c  27451  2lgsoddprmlem2  27467  2lgsoddprm  27474  2sq2  27491  addsq2reu  27498  2sqreultlem  27505  2sqreunnltlem  27508  2sqreulem3  27511  sltval2  27715  sltintdifex  27720  sltres  27721  nosepon  27724  noextenddif  27727  nosepssdm  27745  nogt01o  27755  nosupprefixmo  27759  noinfprefixmo  27760  nosupno  27762  noinfno  27777  sleloe  27813  eqscut2  27865  scutbdaylt  27877  elold  27922  made0  27926  lrrecfr  27990  subadds  28114  cutpw2  28431  renegscl  28444  tgjustf  28495  legtrid  28613  legso  28621  islmib  28809  lmicom  28810  lmiinv  28814  lmimid  28816  lmiopp  28824  colinearalglem2  28936  colinearalg  28939  ax5seglem4  28961  ax5seglem5  28962  axlowdimlem13  28983  axeuclidlem  28991  axeuclid  28992  axcontlem2  28994  axcontlem4  28996  elntg2  29014  structiedg0val  29053  uspgredgiedg  29206  uspgriedgedg  29207  usgredgsscusgredg  29491  fusgrn0degnn0  29531  umgr2v2evtxel  29554  vdiscusgrb  29562  uspgr2wlkeq  29678  wlk0prc  29686  wlklenvclwlk  29687  wlkp1lem8  29712  spthdep  29766  usgr2pthlem  29795  usgr2pth  29796  wlkiswwlksupgr2  29906  wlklnwwlkln2lem  29911  wwlksnextproplem3  29940  umgr2adedgwlk  29974  umgr2adedgspth  29977  umgr2wlkon  29979  umgrwwlks2on  29986  elwwlks2  29995  elwspths2spth  29996  clwlkclwwlklem2a4  30025  clwlkclwwlklem2  30028  erclwwlkref  30048  clwwlkf  30075  erclwwlknref  30097  erclwwlknsym  30098  erclwwlkntr  30099  hashecclwwlkn1  30105  umgrhashecclwwlk  30106  eupth2lem2  30247  eucrct2eupth  30273  numclwwlkqhash  30403  isgrpo  30525  hvsubaddi  31094  hire  31122  shmodsi  31417  omlsilem  31430  chcon1i  31493  chnlei  31513  pjoml3i  31614  cmbr2i  31624  chscllem2  31666  adjsym  31861  eigorthi  31865  dfadj2  31913  adjval2  31919  cnvadj  31920  dmadjrnb  31934  adjvalval  31965  cnlnadjeui  32105  cnlnssadj  32108  adjbdln  32111  pjimai  32204  pjin2i  32221  pjin3i  32222  stadd3i  32276  largei  32295  cvnbtwn3  32316  cvnbtwn4  32317  mddmd2  32337  superpos  32382  atnemeq0  32405  sumdmdii  32443  sumdmdlem  32446  addltmulALT  32474  opreu2reuALT  32504  foresf1o  32531  difeq  32545  disjrdx  32610  fcoinvbr  32624  brab2d  32626  fmptco1f1o  32649  dfimafnf  32652  funcnvmpt  32683  curry2ima  32723  intimafv  32725  cnvoprabOLD  32737  elicoelioo  32786  fzo0opth  32812  wrdt2ind  32922  swrdrn3  32924  orngsqr  33313  qusker  33356  dvdsrspss  33394  lsmsnorb  33398  1arithufdlem4  33554  r1pid2OLD  33608  algextdeglem8  33729  zarcls  33834  xrmulc1cn  33890  xrge0iifcnv  33893  ind1a  33999  esumfsup  34050  esumpcvgval  34058  esumcvg  34066  esum2dlem  34072  issgon  34103  eulerpartgbij  34353  eulerpartlemgh  34359  ballotlemsima  34496  bnj1366  34821  bnj553  34890  bnj964  34935  cusgredgex  35105  revwlk  35108  loop1cycl  35121  subfacp1lem3  35166  subfacp1lem5  35168  erdszelem9  35183  prv1n  35415  ply1divalg3  35626  quad3  35654  br6  35736  elintfv  35745  dfon2lem5  35768  dfon2lem8  35771  brbigcup  35879  dfbigcup2  35880  elfix  35884  ellimits  35891  snelsingles  35903  dfiota3  35904  imageval  35911  brapply  35919  brsuccf  35922  funpartlem  35923  brfullfun  35929  dfrecs2  35931  dfrdg4  35932  altopthbg  35949  altopthc  35952  altopthd  35953  altopelaltxp  35957  brsegle  36089  outsideofrflx  36108  elicc3  36299  nn0prpw  36305  opnregcld  36312  cldregopn  36313  fneval  36334  topfneec  36337  knoppndvlem9  36502  bj-elgab  36921  bj-gabima  36922  bj-elsngl  36950  bj-snglc  36951  bj-projval  36978  bj-disj2r  37010  bj-restreg  37081  bj-0int  37083  copsex2b  37122  bj-inftyexpitaudisj  37187  bj-inftyexpidisj  37192  bj-bary1lem1  37293  topdifinffinlem  37329  topdifinfeq  37332  fvineqsnf1  37392  curf  37584  uncf  37585  curunc  37588  unccur  37589  poimirlem2  37608  poimirlem16  37622  poimirlem17  37623  poimirlem19  37625  poimirlem20  37626  poimirlem27  37633  mblfinlem2  37644  mbfresfi  37652  itg2addnclem2  37658  ftc1anclem3  37681  fdc  37731  heibor1  37796  opidonOLD  37838  0rngo  38013  smprngopr  38038  isfldidl  38054  isfldidl2  38055  eqbrb  38213  eqelb  38215  ideq2  38288  relcnveq  38303  n0elqs  38307  disjressuc2  38369  elrelscnveq  38473  disjdmqscossss  38784  lcvnbtwn3  39009  lcvexchlem1  39015  lsatnem0  39026  opcon1b  39179  omllaw2N  39225  cmtbr2N  39234  leatb  39273  cvlsupr2  39324  glbconxN  39360  islln3  39492  llnexatN  39503  islpln3  39515  lplnexatN  39545  islvol3  39558  dalem-cly  39653  isline4N  39759  2llnma3r  39770  poml4N  39935  4atex2  40059  4atex2-0bOLDN  40061  cdlemefrs29bpre0  40378  cdlemftr3  40547  cdlemb3  40588  cdlemg17h  40650  cdlemg17pq  40654  cdlemg19  40666  cdlemg21  40668  tendoex  40957  dva1dim  40967  dihglb2  41324  doch11  41355  dochsordN  41356  lcfrlem9  41532  hlhillcs  41944  lcmineqlem4  42013  aks6d1c7lem2  42162  aks5lem3a  42170  aks5lem6  42173  unitscyglem2  42177  unitscyglem3  42178  metakunt1  42186  metakunt6  42191  metakunt15  42200  metakunt16  42201  addsubeq4com  42293  ef11d  42353  fimgmcyclem  42519  fsuppind  42576  elrfirn  42682  isnacs2  42693  isnacs3  42697  fiphp3d  42806  wopprc  43018  islnm2  43066  kercvrlsm  43071  fgraphopab  43191  tfsconcatlem  43325  tfsconcatrn  43331  tfsconcat0i  43334  tfsconcat0b  43335  tfsconcatrev  43337  oaun3lem1  43363  oadif1lem  43368  oadif1  43369  rp-fakeuninass  43505  snen1g  43513  iscard4  43522  sqrtcval  43630  frege124d  43750  frege129d  43752  frege92  43944  dffrege99  43951  clsk3nimkb  44029  clsk1indlem4  44033  clsk1indlem1  44034  ntrclsiso  44056  ntrclsk3  44059  ntrclsk13  44060  ntrneik4w  44089  extoimad  44153  int-sqdefd  44170  int-sqgeq0d  44175  radcnvrat  44309  bcc0  44335  opelopab4  44548  eqsbc2VD  44837  fzisoeu  45250  iuneqfzuz  45284  supxrleubrnmptf  45400  rexanuz2nf  45442  fsummulc1f  45526  fsumiunss  45530  fmul01lt1lem2  45540  sumnnodd  45585  fnlimfvre2  45632  limsupreuz  45692  limsupvaluz2  45693  liminfvalxr  45738  icccncfext  45842  cncfiooicc  45849  cncfioobdlem  45851  dvmptmulf  45892  dvmptfprodlem  45899  volioc  45927  itgioocnicc  45932  fourierdlem12  46074  fourierdlem20  46082  fourierdlem25  46087  fourierdlem33  46095  fourierdlem42  46104  fourierdlem52  46113  fourierdlem54  46115  fourierdlem57  46118  fourierdlem58  46119  fourierdlem59  46120  fourierdlem63  46124  fourierdlem65  46126  fourierdlem68  46129  fourierdlem73  46134  fourierdlem74  46135  fourierdlem75  46136  fourierdlem80  46141  fourierdlem81  46142  rrndistlt  46245  sge0ltfirpmpt2  46381  sge0pnfmpt  46400  hoidmv1le  46549  hoidmvle  46555  vonioolem2  46636  smflimlem3  46728  euabsneu  46977  funressnfv  46992  aiotaval  47044  reuf1odnf  47056  reuf1od  47057  afvpcfv0  47095  dfafn5a  47109  afvelrnb  47112  afvelrnb0  47113  dfaimafn2  47115  dfatsnafv2  47201  dfatdmfcoafv2  47203  f1oresf1o2  47240  minusmodnep2tmod  47292  0nelsetpreimafv  47314  fargshiftfo  47366  sprsymrelf1  47420  reupr  47446  fmtnorec2lem  47466  fmtnoprmfac1  47489  fmtnoprmfac2  47491  sfprmdvdsmersenne  47527  lighneallem2  47530  dfeven2  47573  dfodd3  47574  odd2np1ALTV  47598  even3prm2  47643  fppr2odd  47655  nnsum3primesgbe  47716  nnsum3primesle9  47718  clnbgrsym  47761  dfvopnbgr2  47776  isuspgrim0  47809  isuspgrimlem  47811  dfgric2  47821  grtriprop  47845  uspgrlimlem3  47892  gpgvtxedg1  47956  0nodd  48013  2nodd  48015  lmod0rng  48072  rngcinvALTV  48119  ringcinvALTV  48153  lcoel0  48273  lindslinindimp2lem4  48306  ldepspr  48318  lincresunit3  48326  nn0sumshdiglemB  48469  nn0sumshdiglem1  48470  rrx2pnedifcoorneorr  48566  eenglngeehlnmlem1  48586  eenglngeehlnmlem2  48587  rrx2linest  48591  rrx2linest2  48593  rrxsphere  48597  line2ylem  48600  line2x  48603  itscnhlc0xyqsol  48614  itschlc0xyqsol1  48615  itsclinecirc0b  48623  2itscp  48630  inlinecirc02plem  48635