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  3498  clel5  3622  eqsbc2  3808  dfss  3924  sspsstri  4058  ssnelpss  4067  ssdifim  4226  disj  4403  disj4  4412  reuprg0  4656  preq1b  4800  invdisj  5081  disjprg  5091  dtruALT  5330  reusv3  5347  opthg2  5426  copsex2g  5440  copsex4g  5442  opcom  5448  opeqsng  5450  opeqpr  5452  snopeqop  5453  propeqop  5454  opthwiener  5461  vopelopabsb  5476  opthprc  5687  elxp3  5689  relop  5797  dmopab3  5866  rnopab3  5902  rncoeq  5927  restidsing  6008  somin1  6086  xpcan  6129  xpcan2  6130  dfrel4v  6143  dmsnn0  6160  reu3op  6244  reuop  6245  opreu2reurex  6246  ordtri2  6346  ordtri2or3  6413  suc11  6420  on0eqel  6436  snsn0non  6437  iota1  6465  iotan0  6476  sniota  6477  mptfnf  6621  fresaunres1  6701  dffn5  6885  fvelrnb  6887  dfimafn2  6890  funimass4  6891  feqmptdf  6897  fnsnfv  6906  dmfco  6923  fndmdif  6980  fneqeql  6984  rexrn  7025  ralrn  7026  elrnrexdmb  7028  dffo4  7041  fssrescdmd  7064  funopsn  7086  ftpg  7094  fprb  7134  ralima  7177  reximaOLD  7179  ralimaOLD  7180  fvclss  7181  dff13  7195  f1eqcocnv  7242  fnssintima  7303  imaeqsexvOLD  7304  riotaeqimp  7336  eusvobj2  7345  f1ocnvfv3  7348  oprabidw  7384  oprabid  7385  oprabv  7413  eloprabga  7462  ovelimab  7531  onmindif2  7747  br1steqg  7953  br2ndeqg  7954  dfoprab3  7996  opiota  8001  f1o2ndf1  8062  soseq  8099  brtpos2  8172  tpossym  8198  mpocurryd  8209  rdglim2  8361  tz7.48lem  8370  oaf1o  8488  omopthi  8586  erth2  8687  brecop  8744  erovlem  8747  ecopovsym  8753  eceqoveq  8756  xpcomco  8991  omxpenlem  9002  mapen  9065  nneneq  9130  unxpdomlem3  9157  unfilem1  9212  mapfien  9317  supgtoreq  9380  wemapsolem  9461  suc11reg  9534  inf3lem2  9544  inf3lem6  9548  ttrcltr  9631  djulf1o  9827  djurf1o  9828  infenaleph  10004  isinfcard  10005  dfac5  10042  cfeq0  10169  cfsuc  10170  ssfin4  10223  fin23lem25  10237  fin23lem22  10240  fin23lem40  10264  fin1a2lem5  10317  axcclem  10370  brdom7disj  10444  brdom6disj  10445  inar1  10688  psslinpr  10944  ltexprlem4  10952  ltsrpr  10990  mulgt0sr  11018  elreal  11044  ltresr  11053  leloe  11221  eqlei2  11246  addsubeq4  11397  subcan2  11408  negcon1  11435  negcon2  11436  addid0  11558  addeq0  11562  divmul2  11802  conjmul  11860  rereccl  11861  creur  12141  creui  12142  nndiv  12193  nn0sub  12453  elnn0z  12503  elznn0  12505  xrleloe  13065  ngtmnft  13087  icoshftf1o  13396  iccf1o  13418  fzen  13463  fzneuz  13530  injresinj  13710  fleqceilz  13777  mod0  13799  modmuladdnn0  13841  modirr  13868  addmodlteq  13872  nn0ennn  13905  hashrabsn01  14299  hashsdom  14307  hashgt12el2  14349  hashbclem  14378  hashfacen  14380  hashf1lem1  14381  hashtpg  14411  tpf1o  14427  fi1uzind  14433  ccatw2s1p1  14562  wrd2ind  14648  cshw1  14747  cshwsexa  14749  scshwfzeqfzo  14752  s2f1o  14842  wwlktovfo  14884  dmtrclfv  14944  cjreb  15049  leabs  15225  reusq0  15391  incexc2  15764  rpnnen2lem12  16153  dvdsval2  16185  dvdsabseq  16243  dvdsflip  16247  odd2np1  16271  oddm1even  16273  sqoddm1div8z  16284  m1exp1  16306  divalglem4  16326  divalglem8  16330  divalgb  16334  modremain  16338  zeqzmulgcd  16440  dfgcd2  16476  lcmfpr  16557  lcmftp  16566  lcmfunsnlem2  16570  divgcdcoprm0  16595  prm2orodd  16621  hashdvds  16705  oddprmdvds  16834  vdwlem12  16923  cshwshashlem1  17026  cshwsiun  17030  initoid  17927  termoid  17928  setcinv  18016  yonedainv  18206  joinfval  18296  joinfval2  18297  meetfval  18310  meetfval2  18311  latnle  18398  sgrp2nmndlem3  18818  grpid  18873  grpinvcnv  18904  grplmulf1o  18911  grpraddf1o  18912  grpsubeq0  18924  grpsubadd  18926  grplactcnv  18941  ressmulgnnd  18976  isnsg4  19065  eqg0el  19081  cycsubmel  19098  conjghm  19147  conjnmzb  19151  gacan  19203  gapm  19204  cntzrec  19234  oppgcntz  19262  fvcosymgeq  19327  odmulgeq  19455  dfod2  19462  sylow3lem3  19527  sylow3lem6  19530  lssnle  19572  lsmhash  19603  efgredlemb  19644  efgrelexlemb  19648  dprd2d2  19944  ablfac1eulem  19972  pgpfac1lem2  19975  pgpfac1lem4  19978  dvdsrval  20265  dvdsr02  20276  01eq0ring  20434  0ring01eqbi  20436  rngcinv  20541  ringcinv  20575  orngsqr  20770  rmodislmodlem  20851  lvecinv  21039  rngqiprngimf1lem  21220  rspsn  21259  dfcnfldOLD  21296  prmirredlem  21398  zndvds  21475  znleval  21480  psrbagconf1o  21855  mplmonmul  21960  gsummoncoe1  22212  evl1maprhm  22283  mat1dimelbas  22375  mat1dimbas  22376  1mavmul  22452  ma1repveval  22475  mulmarep1gsum1  22477  mdetunilem9  22524  m2cpminvid2lem  22658  pmatcollpw3lem  22687  mp2pm2mplem4  22713  toponsspwpw  22826  dmtopon  22827  cmpfi  23312  ssref  23416  qtopeu  23620  hmeoimaf1o  23674  txhmeo  23707  fbasrn  23788  rnelfmlem  23856  hauspwpwf1  23891  alexsubALTlem4  23954  qustgpopn  24024  qustgphaus  24027  fmucndlem  24195  isngp3  24503  isngp4  24517  metnrmlem1a  24764  icopnfcnv  24857  iccpnfcnv  24859  ivthle  25374  ivthle2  25375  dyadmbl  25518  mbfinf  25583  i1fmulclem  25620  itg1mulc  25622  mvth  25914  dvivth  25932  lhop2  25937  r1pid2  26084  dvdsq1p  26085  reeff1o  26374  coseq1  26451  recosf1o  26461  resinf1o  26462  efopn  26584  cxpeq  26684  logreclem  26689  affineequiv  26750  affineequiv4  26753  affineequivne  26754  quad2  26766  dcubic  26773  mcubic  26774  quart  26788  atandm2  26804  rlimcnp2  26893  amgm  26918  wilthlem2  26996  mumullem2  27107  sqff1o  27109  dvdsflf1o  27114  gausslemma2dlem0i  27292  lgseisenlem2  27304  lgsquadlem2  27309  2lgslem1c  27321  2lgsoddprmlem2  27337  2lgsoddprm  27344  2sq2  27361  addsq2reu  27368  2sqreultlem  27375  2sqreunnltlem  27378  2sqreulem3  27381  sltval2  27585  sltintdifex  27590  sltres  27591  nosepon  27594  noextenddif  27597  nosepssdm  27615  nogt01o  27625  nosupprefixmo  27629  noinfprefixmo  27630  nosupno  27632  noinfno  27647  sleloe  27683  eqscut2  27736  scutbdaylt  27748  elold  27802  made0  27806  lrrecfr  27874  subadds  27998  onscutlt  28189  zs12ge0  28379  renegscl  28386  tgjustf  28437  legtrid  28555  legso  28563  islmib  28751  lmicom  28752  lmiinv  28756  lmimid  28758  lmiopp  28766  colinearalglem2  28871  colinearalg  28874  ax5seglem4  28896  ax5seglem5  28897  axlowdimlem13  28918  axeuclidlem  28926  axeuclid  28927  axcontlem2  28929  axcontlem4  28931  elntg2  28949  structiedg0val  28986  uspgredgiedg  29139  uspgriedgedg  29140  usgredgsscusgredg  29424  fusgrn0degnn0  29464  umgr2v2evtxel  29487  vdiscusgrb  29495  uspgr2wlkeq  29610  wlk0prc  29617  wlklenvclwlk  29618  wlkp1lem8  29643  spthdep  29698  usgr2pthlem  29727  usgr2pth  29728  wlkiswwlksupgr2  29841  wlklnwwlkln2lem  29846  wwlksnextproplem3  29875  umgr2adedgwlk  29909  umgr2adedgspth  29912  umgr2wlkon  29914  umgrwwlks2on  29921  elwwlks2  29930  elwspths2spth  29931  clwlkclwwlklem2a4  29960  clwlkclwwlklem2  29963  erclwwlkref  29983  clwwlkf  30010  erclwwlknref  30032  erclwwlknsym  30033  erclwwlkntr  30034  hashecclwwlkn1  30040  umgrhashecclwwlk  30041  eupth2lem2  30182  eucrct2eupth  30208  numclwwlkqhash  30338  isgrpo  30460  hvsubaddi  31029  hire  31057  shmodsi  31352  omlsilem  31365  chcon1i  31428  chnlei  31448  pjoml3i  31549  cmbr2i  31559  chscllem2  31601  adjsym  31796  eigorthi  31800  dfadj2  31848  adjval2  31854  cnvadj  31855  dmadjrnb  31869  adjvalval  31900  cnlnadjeui  32040  cnlnssadj  32043  adjbdln  32046  pjimai  32139  pjin2i  32156  pjin3i  32157  stadd3i  32211  largei  32230  cvnbtwn3  32251  cvnbtwn4  32252  mddmd2  32272  superpos  32317  atnemeq0  32340  sumdmdii  32378  sumdmdlem  32381  addltmulALT  32409  opreu2reuALT  32440  foresf1o  32467  difeq  32481  disjrdx  32554  fcoinvbr  32568  brab2d  32571  fmptco1f1o  32595  dfimafnf  32598  funcnvmpt  32629  curry2ima  32670  intimafv  32672  receqid  32707  elicoelioo  32740  fzo0opth  32767  ind1a  32821  wrdt2ind  32914  swrdrn3  32916  cntrval2  33132  qusker  33305  dvdsrspss  33343  lsmsnorb  33347  1arithufdlem4  33503  r1pid2OLD  33560  algextdeglem8  33710  zarcls  33860  xrmulc1cn  33916  xrge0iifcnv  33919  esumfsup  34056  esumpcvgval  34064  esumcvg  34072  esum2dlem  34078  issgon  34109  eulerpartgbij  34359  eulerpartlemgh  34365  ballotlemsima  34503  bnj1366  34815  bnj553  34884  bnj964  34929  cusgredgex  35114  revwlk  35117  loop1cycl  35129  subfacp1lem3  35174  subfacp1lem5  35176  erdszelem9  35191  prv1n  35423  ply1divalg3  35634  quad3  35662  br6  35749  elintfv  35757  dfon2lem5  35780  dfon2lem8  35783  brbigcup  35891  dfbigcup2  35892  elfix  35896  ellimits  35903  snelsingles  35915  dfiota3  35916  imageval  35923  brapply  35931  brsuccf  35934  funpartlem  35935  brfullfun  35941  dfrecs2  35943  dfrdg4  35944  altopthbg  35961  altopthc  35964  altopthd  35965  altopelaltxp  35969  brsegle  36101  outsideofrflx  36120  elicc3  36310  nn0prpw  36316  opnregcld  36323  cldregopn  36324  fneval  36345  topfneec  36348  knoppndvlem9  36513  bj-elgab  36932  bj-gabima  36933  bj-elsngl  36961  bj-snglc  36962  bj-projval  36989  bj-disj2r  37021  bj-restreg  37092  bj-0int  37094  copsex2b  37133  bj-inftyexpitaudisj  37198  bj-inftyexpidisj  37203  bj-bary1lem1  37304  topdifinffinlem  37340  topdifinfeq  37343  fvineqsnf1  37403  curf  37597  uncf  37598  curunc  37601  unccur  37602  poimirlem2  37621  poimirlem16  37635  poimirlem17  37636  poimirlem19  37638  poimirlem20  37639  poimirlem27  37646  mblfinlem2  37657  mbfresfi  37665  itg2addnclem2  37671  ftc1anclem3  37694  fdc  37744  heibor1  37809  opidonOLD  37851  0rngo  38026  smprngopr  38051  isfldidl  38067  isfldidl2  38068  eqbrb  38226  eqelb  38228  ideq2  38300  relcnveq  38315  n0elqs  38319  disjressuc2  38379  elrelscnveq  38488  qseq  38645  disjdmqscossss  38800  lcvnbtwn3  39026  lcvexchlem1  39032  lsatnem0  39043  opcon1b  39196  omllaw2N  39242  cmtbr2N  39251  leatb  39290  cvlsupr2  39341  glbconxN  39377  islln3  39509  llnexatN  39520  islpln3  39532  lplnexatN  39562  islvol3  39575  dalem-cly  39670  isline4N  39776  2llnma3r  39787  poml4N  39952  4atex2  40076  4atex2-0bOLDN  40078  cdlemefrs29bpre0  40395  cdlemftr3  40564  cdlemb3  40605  cdlemg17h  40667  cdlemg17pq  40671  cdlemg19  40683  cdlemg21  40685  tendoex  40974  dva1dim  40984  dihglb2  41341  doch11  41372  dochsordN  41373  lcfrlem9  41549  hlhillcs  41957  lcmineqlem4  42025  aks6d1c7lem2  42174  aks5lem3a  42182  aks5lem6  42185  unitscyglem2  42189  unitscyglem3  42190  addsubeq4com  42273  ef11d  42332  fimgmcyclem  42526  fsuppind  42583  elrfirn  42688  isnacs2  42699  isnacs3  42703  fiphp3d  42812  wopprc  43023  islnm2  43071  kercvrlsm  43076  fgraphopab  43196  tfsconcatlem  43329  tfsconcatrn  43335  tfsconcat0i  43338  tfsconcat0b  43339  tfsconcatrev  43341  oaun3lem1  43367  oadif1lem  43372  oadif1  43373  rp-fakeuninass  43509  snen1g  43517  iscard4  43526  sqrtcval  43634  frege124d  43754  frege129d  43756  frege92  43948  dffrege99  43955  clsk3nimkb  44033  clsk1indlem4  44037  clsk1indlem1  44038  ntrclsiso  44060  ntrclsk3  44063  ntrclsk13  44064  ntrneik4w  44093  extoimad  44157  int-sqdefd  44174  int-sqgeq0d  44179  radcnvrat  44307  bcc0  44333  opelopab4  44545  eqsbc2VD  44833  fzisoeu  45302  iuneqfzuz  45335  supxrleubrnmptf  45450  rexanuz2nf  45491  fsummulc1f  45572  fsumiunss  45576  fmul01lt1lem2  45586  sumnnodd  45631  fnlimfvre2  45678  limsupreuz  45738  limsupvaluz2  45739  liminfvalxr  45784  icccncfext  45888  cncfiooicc  45895  cncfioobdlem  45897  dvmptmulf  45938  dvmptfprodlem  45945  volioc  45973  itgioocnicc  45978  fourierdlem12  46120  fourierdlem20  46128  fourierdlem25  46133  fourierdlem33  46141  fourierdlem42  46150  fourierdlem52  46159  fourierdlem54  46161  fourierdlem57  46164  fourierdlem58  46165  fourierdlem59  46166  fourierdlem63  46170  fourierdlem65  46172  fourierdlem68  46175  fourierdlem73  46180  fourierdlem74  46181  fourierdlem75  46182  fourierdlem80  46187  fourierdlem81  46188  rrndistlt  46291  sge0ltfirpmpt2  46427  sge0pnfmpt  46446  hoidmv1le  46595  hoidmvle  46601  vonioolem2  46682  smflimlem3  46774  lambert0  46891  lamberte  46892  euabsneu  47032  funressnfv  47047  aiotaval  47099  reuf1odnf  47111  reuf1od  47112  afvpcfv0  47150  dfafn5a  47164  afvelrnb  47167  afvelrnb0  47168  dfaimafn2  47170  dfatsnafv2  47256  dfatdmfcoafv2  47258  f1oresf1o2  47295  ceilbi  47337  minusmodnep2tmod  47357  0nelsetpreimafv  47394  fargshiftfo  47446  sprsymrelf1  47500  reupr  47526  fmtnorec2lem  47546  fmtnoprmfac1  47569  fmtnoprmfac2  47571  sfprmdvdsmersenne  47607  lighneallem2  47610  dfeven2  47653  dfodd3  47654  odd2np1ALTV  47678  even3prm2  47723  fppr2odd  47735  nnsum3primesgbe  47796  nnsum3primesle9  47798  clnbgrsym  47842  dfvopnbgr2  47857  isuspgrim0  47898  isuspgrimlem  47899  dfgric2  47919  grtriprop  47945  uspgrlimlem3  47994  gpgvtxedg1  48068  pgnbgreunbgrlem2lem1  48118  pgnbgreunbgrlem2lem2  48119  0nodd  48174  2nodd  48176  lmod0rng  48233  rngcinvALTV  48280  ringcinvALTV  48314  lcoel0  48433  lindslinindimp2lem4  48466  ldepspr  48478  lincresunit3  48486  nn0sumshdiglemB  48625  nn0sumshdiglem1  48626  rrx2pnedifcoorneorr  48722  eenglngeehlnmlem1  48742  eenglngeehlnmlem2  48743  rrx2linest  48747  rrx2linest2  48749  rrxsphere  48753  line2ylem  48756  line2x  48759  itscnhlc0xyqsol  48770  itschlc0xyqsol1  48771  itsclinecirc0b  48779  2itscp  48786  inlinecirc02plem  48791  brab2dd  48832  uptr2  49226