Theorem eqcom 2736

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

Syntax hints:   ↔ wb 206   = wceq 1540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721

This theorem is referenced by:  eqcoms  2737  eqcomi  2738  neqcomd  2739  eqeq2d  2740  eqabcb  2869  necom  2978  nesym  2981  gencbvex  3504  clel5  3628  eqsbc2  3814  dfss  3930  sspsstri  4064  ssnelpss  4073  ssdifim  4232  disj  4409  disj4  4418  reuprg0  4662  preq1b  4806  invdisj  5088  disjprg  5098  dtruALT  5338  reusv3  5355  opthg2  5434  copsex2g  5448  copsex4g  5450  opcom  5456  opeqsng  5458  opeqpr  5460  snopeqop  5461  propeqop  5462  opthwiener  5469  vopelopabsb  5484  opthprc  5695  elxp3  5697  relop  5804  dmopab3  5873  rnopab3  5909  rncoeq  5932  restidsing  6013  somin1  6094  xpcan  6137  xpcan2  6138  dfrel4v  6151  dmsnn0  6168  reu3op  6253  reuop  6254  opreu2reurex  6255  ordtri2  6355  ordtri2or3  6422  suc11  6429  on0eqel  6446  snsn0non  6447  iota1  6476  iotan0  6489  sniota  6490  mptfnf  6635  fresaunres1  6715  dffn5  6901  fvelrnb  6903  dfimafn2  6906  funimass4  6907  feqmptdf  6913  fnsnfv  6922  dmfco  6939  fndmdif  6996  fneqeql  7000  rexrn  7041  ralrn  7042  elrnrexdmb  7044  dffo4  7057  fssrescdmd  7080  funopsn  7102  ftpg  7110  fprb  7150  ralima  7193  reximaOLD  7195  ralimaOLD  7196  fvclss  7197  dff13  7211  f1eqcocnv  7258  fnssintima  7319  imaeqsexvOLD  7320  riotaeqimp  7352  eusvobj2  7361  f1ocnvfv3  7364  oprabidw  7400  oprabid  7401  oprabv  7429  eloprabga  7478  ovelimab  7547  onmindif2  7763  br1steqg  7969  br2ndeqg  7970  dfoprab3  8012  opiota  8017  f1o2ndf1  8078  soseq  8115  brtpos2  8188  tpossym  8214  mpocurryd  8225  rdglim2  8377  tz7.48lem  8386  oaf1o  8504  omopthi  8602  erth2  8703  brecop  8760  erovlem  8763  ecopovsym  8769  eceqoveq  8772  xpcomco  9008  omxpenlem  9019  mapen  9082  nneneq  9147  unxpdomlem3  9175  unfilem1  9230  mapfien  9335  supgtoreq  9398  wemapsolem  9479  suc11reg  9548  inf3lem2  9558  inf3lem6  9562  ttrcltr  9645  djulf1o  9841  djurf1o  9842  infenaleph  10020  isinfcard  10021  dfac5  10058  cfeq0  10185  cfsuc  10186  ssfin4  10239  fin23lem25  10253  fin23lem22  10256  fin23lem40  10280  fin1a2lem5  10333  axcclem  10386  brdom7disj  10460  brdom6disj  10461  inar1  10704  psslinpr  10960  ltexprlem4  10968  ltsrpr  11006  mulgt0sr  11034  elreal  11060  ltresr  11069  leloe  11236  eqlei2  11261  addsubeq4  11412  subcan2  11423  negcon1  11450  negcon2  11451  addid0  11573  addeq0  11577  divmul2  11817  conjmul  11875  rereccl  11876  creur  12156  creui  12157  nndiv  12208  nn0sub  12468  elnn0z  12518  elznn0  12520  xrleloe  13080  ngtmnft  13102  icoshftf1o  13411  iccf1o  13433  fzen  13478  fzneuz  13545  injresinj  13725  fleqceilz  13792  mod0  13814  modmuladdnn0  13856  modirr  13883  addmodlteq  13887  nn0ennn  13920  hashrabsn01  14314  hashsdom  14322  hashgt12el2  14364  hashbclem  14393  hashfacen  14395  hashf1lem1  14396  hashtpg  14426  tpf1o  14442  fi1uzind  14448  ccatw2s1p1  14577  wrd2ind  14664  cshw1  14763  cshwsexa  14765  scshwfzeqfzo  14768  s2f1o  14858  wwlktovfo  14900  dmtrclfv  14960  cjreb  15065  leabs  15241  reusq0  15407  incexc2  15780  rpnnen2lem12  16169  dvdsval2  16201  dvdsabseq  16259  dvdsflip  16263  odd2np1  16287  oddm1even  16289  sqoddm1div8z  16300  m1exp1  16322  divalglem4  16342  divalglem8  16346  divalgb  16350  modremain  16354  zeqzmulgcd  16456  dfgcd2  16492  lcmfpr  16573  lcmftp  16582  lcmfunsnlem2  16586  divgcdcoprm0  16611  prm2orodd  16637  hashdvds  16721  oddprmdvds  16850  vdwlem12  16939  cshwshashlem1  17042  cshwsiun  17046  initoid  17939  termoid  17940  setcinv  18028  yonedainv  18218  joinfval  18308  joinfval2  18309  meetfval  18322  meetfval2  18323  latnle  18408  sgrp2nmndlem3  18828  grpid  18883  grpinvcnv  18914  grplmulf1o  18921  grpraddf1o  18922  grpsubeq0  18934  grpsubadd  18936  grplactcnv  18951  ressmulgnnd  18986  isnsg4  19075  eqg0el  19091  cycsubmel  19108  conjghm  19157  conjnmzb  19161  gacan  19213  gapm  19214  cntzrec  19244  oppgcntz  19272  fvcosymgeq  19335  odmulgeq  19463  dfod2  19470  sylow3lem3  19535  sylow3lem6  19538  lssnle  19580  lsmhash  19611  efgredlemb  19652  efgrelexlemb  19656  dprd2d2  19952  ablfac1eulem  19980  pgpfac1lem2  19983  pgpfac1lem4  19986  dvdsrval  20246  dvdsr02  20257  01eq0ring  20415  0ring01eqbi  20417  rngcinv  20522  ringcinv  20556  rmodislmodlem  20811  lvecinv  20999  rngqiprngimf1lem  21180  rspsn  21219  dfcnfldOLD  21256  prmirredlem  21358  zndvds  21435  znleval  21440  psrbagconf1o  21814  mplmonmul  21919  gsummoncoe1  22171  evl1maprhm  22242  mat1dimelbas  22334  mat1dimbas  22335  1mavmul  22411  ma1repveval  22434  mulmarep1gsum1  22436  mdetunilem9  22483  m2cpminvid2lem  22617  pmatcollpw3lem  22646  mp2pm2mplem4  22672  toponsspwpw  22785  dmtopon  22786  cmpfi  23271  ssref  23375  qtopeu  23579  hmeoimaf1o  23633  txhmeo  23666  fbasrn  23747  rnelfmlem  23815  hauspwpwf1  23850  alexsubALTlem4  23913  qustgpopn  23983  qustgphaus  23986  fmucndlem  24154  isngp3  24462  isngp4  24476  metnrmlem1a  24723  icopnfcnv  24816  iccpnfcnv  24818  ivthle  25333  ivthle2  25334  dyadmbl  25477  mbfinf  25542  i1fmulclem  25579  itg1mulc  25581  mvth  25873  dvivth  25891  lhop2  25896  r1pid2  26043  dvdsq1p  26044  reeff1o  26333  coseq1  26410  recosf1o  26420  resinf1o  26421  efopn  26543  cxpeq  26643  logreclem  26648  affineequiv  26709  affineequiv4  26712  affineequivne  26713  quad2  26725  dcubic  26732  mcubic  26733  quart  26747  atandm2  26763  rlimcnp2  26852  amgm  26877  wilthlem2  26955  mumullem2  27066  sqff1o  27068  dvdsflf1o  27073  gausslemma2dlem0i  27251  lgseisenlem2  27263  lgsquadlem2  27268  2lgslem1c  27280  2lgsoddprmlem2  27296  2lgsoddprm  27303  2sq2  27320  addsq2reu  27327  2sqreultlem  27334  2sqreunnltlem  27337  2sqreulem3  27340  sltval2  27544  sltintdifex  27549  sltres  27550  nosepon  27553  noextenddif  27556  nosepssdm  27574  nogt01o  27584  nosupprefixmo  27588  noinfprefixmo  27589  nosupno  27591  noinfno  27606  sleloe  27642  eqscut2  27694  scutbdaylt  27706  elold  27757  made0  27761  lrrecfr  27826  subadds  27950  onscutlt  28141  zs12ge0  28318  renegscl  28325  tgjustf  28376  legtrid  28494  legso  28502  islmib  28690  lmicom  28691  lmiinv  28695  lmimid  28697  lmiopp  28705  colinearalglem2  28810  colinearalg  28813  ax5seglem4  28835  ax5seglem5  28836  axlowdimlem13  28857  axeuclidlem  28865  axeuclid  28866  axcontlem2  28868  axcontlem4  28870  elntg2  28888  structiedg0val  28925  uspgredgiedg  29078  uspgriedgedg  29079  usgredgsscusgredg  29363  fusgrn0degnn0  29403  umgr2v2evtxel  29426  vdiscusgrb  29434  uspgr2wlkeq  29549  wlk0prc  29556  wlklenvclwlk  29557  wlkp1lem8  29582  spthdep  29637  usgr2pthlem  29666  usgr2pth  29667  wlkiswwlksupgr2  29780  wlklnwwlkln2lem  29785  wwlksnextproplem3  29814  umgr2adedgwlk  29848  umgr2adedgspth  29851  umgr2wlkon  29853  umgrwwlks2on  29860  elwwlks2  29869  elwspths2spth  29870  clwlkclwwlklem2a4  29899  clwlkclwwlklem2  29902  erclwwlkref  29922  clwwlkf  29949  erclwwlknref  29971  erclwwlknsym  29972  erclwwlkntr  29973  hashecclwwlkn1  29979  umgrhashecclwwlk  29980  eupth2lem2  30121  eucrct2eupth  30147  numclwwlkqhash  30277  isgrpo  30399  hvsubaddi  30968  hire  30996  shmodsi  31291  omlsilem  31304  chcon1i  31367  chnlei  31387  pjoml3i  31488  cmbr2i  31498  chscllem2  31540  adjsym  31735  eigorthi  31739  dfadj2  31787  adjval2  31793  cnvadj  31794  dmadjrnb  31808  adjvalval  31839  cnlnadjeui  31979  cnlnssadj  31982  adjbdln  31985  pjimai  32078  pjin2i  32095  pjin3i  32096  stadd3i  32150  largei  32169  cvnbtwn3  32190  cvnbtwn4  32191  mddmd2  32211  superpos  32256  atnemeq0  32279  sumdmdii  32317  sumdmdlem  32320  addltmulALT  32348  opreu2reuALT  32379  foresf1o  32406  difeq  32420  disjrdx  32493  fcoinvbr  32507  brab2d  32508  fmptco1f1o  32530  dfimafnf  32533  funcnvmpt  32564  curry2ima  32605  intimafv  32607  receqid  32641  elicoelioo  32674  fzo0opth  32701  ind1a  32755  wrdt2ind  32848  swrdrn3  32850  cntrval2  33101  orngsqr  33255  qusker  33293  dvdsrspss  33331  lsmsnorb  33335  1arithufdlem4  33491  r1pid2OLD  33547  algextdeglem8  33687  zarcls  33837  xrmulc1cn  33893  xrge0iifcnv  33896  esumfsup  34033  esumpcvgval  34041  esumcvg  34049  esum2dlem  34055  issgon  34086  eulerpartgbij  34336  eulerpartlemgh  34342  ballotlemsima  34480  bnj1366  34792  bnj553  34861  bnj964  34906  cusgredgex  35082  revwlk  35085  loop1cycl  35097  subfacp1lem3  35142  subfacp1lem5  35144  erdszelem9  35159  prv1n  35391  ply1divalg3  35602  quad3  35630  br6  35717  elintfv  35725  dfon2lem5  35748  dfon2lem8  35751  brbigcup  35859  dfbigcup2  35860  elfix  35864  ellimits  35871  snelsingles  35883  dfiota3  35884  imageval  35891  brapply  35899  brsuccf  35902  funpartlem  35903  brfullfun  35909  dfrecs2  35911  dfrdg4  35912  altopthbg  35929  altopthc  35932  altopthd  35933  altopelaltxp  35937  brsegle  36069  outsideofrflx  36088  elicc3  36278  nn0prpw  36284  opnregcld  36291  cldregopn  36292  fneval  36313  topfneec  36316  knoppndvlem9  36481  bj-elgab  36900  bj-gabima  36901  bj-elsngl  36929  bj-snglc  36930  bj-projval  36957  bj-disj2r  36989  bj-restreg  37060  bj-0int  37062  copsex2b  37101  bj-inftyexpitaudisj  37166  bj-inftyexpidisj  37171  bj-bary1lem1  37272  topdifinffinlem  37308  topdifinfeq  37311  fvineqsnf1  37371  curf  37565  uncf  37566  curunc  37569  unccur  37570  poimirlem2  37589  poimirlem16  37603  poimirlem17  37604  poimirlem19  37606  poimirlem20  37607  poimirlem27  37614  mblfinlem2  37625  mbfresfi  37633  itg2addnclem2  37639  ftc1anclem3  37662  fdc  37712  heibor1  37777  opidonOLD  37819  0rngo  37994  smprngopr  38019  isfldidl  38035  isfldidl2  38036  eqbrb  38194  eqelb  38196  ideq2  38268  relcnveq  38283  n0elqs  38287  disjressuc2  38347  elrelscnveq  38456  qseq  38613  disjdmqscossss  38768  lcvnbtwn3  38994  lcvexchlem1  39000  lsatnem0  39011  opcon1b  39164  omllaw2N  39210  cmtbr2N  39219  leatb  39258  cvlsupr2  39309  glbconxN  39345  islln3  39477  llnexatN  39488  islpln3  39500  lplnexatN  39530  islvol3  39543  dalem-cly  39638  isline4N  39744  2llnma3r  39755  poml4N  39920  4atex2  40044  4atex2-0bOLDN  40046  cdlemefrs29bpre0  40363  cdlemftr3  40532  cdlemb3  40573  cdlemg17h  40635  cdlemg17pq  40639  cdlemg19  40651  cdlemg21  40653  tendoex  40942  dva1dim  40952  dihglb2  41309  doch11  41340  dochsordN  41341  lcfrlem9  41517  hlhillcs  41925  lcmineqlem4  41993  aks6d1c7lem2  42142  aks5lem3a  42150  aks5lem6  42153  unitscyglem2  42157  unitscyglem3  42158  addsubeq4com  42241  ef11d  42300  fimgmcyclem  42494  fsuppind  42551  elrfirn  42656  isnacs2  42667  isnacs3  42671  fiphp3d  42780  wopprc  42992  islnm2  43040  kercvrlsm  43045  fgraphopab  43165  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  44276  bcc0  44302  opelopab4  44514  eqsbc2VD  44802  fzisoeu  45271  iuneqfzuz  45304  supxrleubrnmptf  45420  rexanuz2nf  45461  fsummulc1f  45542  fsumiunss  45546  fmul01lt1lem2  45556  sumnnodd  45601  fnlimfvre2  45648  limsupreuz  45708  limsupvaluz2  45709  liminfvalxr  45754  icccncfext  45858  cncfiooicc  45865  cncfioobdlem  45867  dvmptmulf  45908  dvmptfprodlem  45915  volioc  45943  itgioocnicc  45948  fourierdlem12  46090  fourierdlem20  46098  fourierdlem25  46103  fourierdlem33  46111  fourierdlem42  46120  fourierdlem52  46129  fourierdlem54  46131  fourierdlem57  46134  fourierdlem58  46135  fourierdlem59  46136  fourierdlem63  46140  fourierdlem65  46142  fourierdlem68  46145  fourierdlem73  46150  fourierdlem74  46151  fourierdlem75  46152  fourierdlem80  46157  fourierdlem81  46158  rrndistlt  46261  sge0ltfirpmpt2  46397  sge0pnfmpt  46416  hoidmv1le  46565  hoidmvle  46571  vonioolem2  46652  smflimlem3  46744  lambert0  46861  lamberte  46862  euabsneu  47002  funressnfv  47017  aiotaval  47069  reuf1odnf  47081  reuf1od  47082  afvpcfv0  47120  dfafn5a  47134  afvelrnb  47137  afvelrnb0  47138  dfaimafn2  47140  dfatsnafv2  47226  dfatdmfcoafv2  47228  f1oresf1o2  47265  ceilbi  47307  minusmodnep2tmod  47327  0nelsetpreimafv  47364  fargshiftfo  47416  sprsymrelf1  47470  reupr  47496  fmtnorec2lem  47516  fmtnoprmfac1  47539  fmtnoprmfac2  47541  sfprmdvdsmersenne  47577  lighneallem2  47580  dfeven2  47623  dfodd3  47624  odd2np1ALTV  47648  even3prm2  47693  fppr2odd  47705  nnsum3primesgbe  47766  nnsum3primesle9  47768  clnbgrsym  47811  dfvopnbgr2  47826  isuspgrim0  47867  isuspgrimlem  47868  dfgric2  47888  grtriprop  47913  uspgrlimlem3  47962  gpgvtxedg1  48028  pgnbgreunbgrlem2lem1  48077  pgnbgreunbgrlem2lem2  48078  0nodd  48131  2nodd  48133  lmod0rng  48190  rngcinvALTV  48237  ringcinvALTV  48271  lcoel0  48390  lindslinindimp2lem4  48423  ldepspr  48435  lincresunit3  48443  nn0sumshdiglemB  48582  nn0sumshdiglem1  48583  rrx2pnedifcoorneorr  48679  eenglngeehlnmlem1  48699  eenglngeehlnmlem2  48700  rrx2linest  48704  rrx2linest2  48706  rrxsphere  48710  line2ylem  48713  line2x  48716  itscnhlc0xyqsol  48727  itschlc0xyqsol1  48728  itsclinecirc0b  48736  2itscp  48743  inlinecirc02plem  48748  brab2dd  48789  uptr2  49183