Theorem eqcom 2738

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

Syntax hints:   ↔ wb 205   = wceq 1540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-9 2115  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1781  df-cleq 2723

This theorem is referenced by:  eqcoms  2739  eqcomi  2740  neqcomd  2741  eqeq2d  2742  eqtr2OLD  2756  eqtr3OLD  2758  eqabcb  2874  necom  2993  nesym  2996  pm13.181OLD  3023  gencbvex  3535  clel5  3655  eqsbc2  3846  dfss  3966  sspsstri  4102  ssnelpss  4111  ssdifim  4262  disj  4447  disj4  4458  reuprg0  4706  preq1b  4847  invdisj  5132  disjprgw  5143  disjprg  5144  dtruALT  5386  reusv3  5403  opthg2  5479  copsex2g  5493  copsex4g  5495  opcom  5501  opeqsng  5503  opeqpr  5505  snopeqop  5506  propeqop  5507  opthwiener  5514  vopelopabsb  5529  opthprc  5740  elxp3  5742  relop  5850  dmopab3  5919  rncoeq  5974  restidsing  6052  somin1  6134  xpcan  6175  xpcan2  6176  dfrel4v  6189  dmsnn0  6206  reu3op  6291  reuop  6292  opreu2reurex  6293  ordtri2  6399  ordtri2or3  6464  suc11  6471  on0eqel  6488  snsn0non  6489  iota1  6520  iotan0  6533  sniota  6534  mptfnf  6685  fresaunres1  6764  dffn5  6950  fvelrnb  6952  dfimafn2  6955  funimass4  6956  feqmptdf  6962  fnsnfv  6970  fnsnfvOLD  6971  dmfco  6987  fndmdif  7043  fneqeql  7047  rexrn  7088  ralrn  7089  elrnrexdmb  7091  dffo4  7104  funopsn  7148  ftpg  7156  fprb  7197  rexima  7241  ralima  7242  fvclss  7243  dff13  7257  f1eqcocnv  7302  f1eqcocnvOLD  7303  fnssintima  7362  imaeqsexv  7363  riotaeqimp  7395  eusvobj2  7404  f1ocnvfv3  7407  oprabidw  7443  oprabid  7444  oprabv  7472  eloprabga  7519  eloprabgaOLD  7520  ovelimab  7589  onmindif2  7799  br1steqg  8001  br2ndeqg  8002  dfoprab3  8044  opiota  8049  f1o2ndf1  8113  soseq  8150  brtpos2  8223  tpossym  8249  mpocurryd  8260  rdglim2  8438  tz7.48lem  8447  oaf1o  8569  omopthi  8666  erth2  8759  brecop  8810  erovlem  8813  ecopovsym  8819  eceqoveq  8822  xpcomco  9068  omxpenlem  9079  mapen  9147  nneneq  9215  nneneqOLD  9227  unxpdomlem3  9258  unfilem1  9316  mapfien  9409  supgtoreq  9471  wemapsolem  9551  suc11reg  9620  inf3lem2  9630  inf3lem6  9634  ttrcltr  9717  djulf1o  9913  djurf1o  9914  infenaleph  10092  isinfcard  10093  dfac5  10129  cfeq0  10257  cfsuc  10258  ssfin4  10311  fin23lem25  10325  fin23lem22  10328  fin23lem40  10352  fin1a2lem5  10405  axcclem  10458  brdom7disj  10532  brdom6disj  10533  inar1  10776  psslinpr  11032  ltexprlem4  11040  ltsrpr  11078  mulgt0sr  11106  elreal  11132  ltresr  11141  leloe  11307  eqlei2  11332  addsubeq4  11482  subcan2  11492  negcon1  11519  negcon2  11520  addid0  11640  addeq0  11644  divmul2  11883  conjmul  11938  rereccl  11939  creur  12213  creui  12214  nndiv  12265  nn0sub  12529  elnn0z  12578  elznn0  12580  xrleloe  13130  ngtmnft  13152  icoshftf1o  13458  iccf1o  13480  fzen  13525  fzneuz  13589  injresinj  13760  fleqceilz  13826  mod0  13848  modmuladdnn0  13887  modirr  13914  addmodlteq  13918  nn0ennn  13951  hashrabsn01  14340  hashsdom  14348  hashgt12el2  14390  hashbclem  14418  hashfacen  14420  hashfacenOLD  14421  hashf1lem1  14422  hashf1lem1OLD  14423  hashtpg  14453  fi1uzind  14465  ccatw2s1p1  14593  wrd2ind  14680  cshw1  14779  cshwsexa  14781  scshwfzeqfzo  14784  s2f1o  14874  wwlktovfo  14916  dmtrclfv  14972  cjreb  15077  leabs  15253  reusq0  15416  incexc2  15791  rpnnen2lem12  16175  dvdsval2  16207  dvdsabseq  16263  dvdsflip  16267  odd2np1  16291  oddm1even  16293  sqoddm1div8z  16304  m1exp1  16326  divalglem4  16346  divalglem8  16350  divalgb  16354  modremain  16358  zeqzmulgcd  16458  dfgcd2  16495  lcmfpr  16571  lcmftp  16580  lcmfunsnlem2  16584  divgcdcoprm0  16609  prm2orodd  16635  hashdvds  16715  oddprmdvds  16843  vdwlem12  16932  cshwshashlem1  17036  cshwsiun  17040  initoid  17961  termoid  17962  setcinv  18050  yonedainv  18244  joinfval  18336  joinfval2  18337  meetfval  18350  meetfval2  18351  latnle  18436  sgrp2nmndlem3  18848  grpid  18903  grpinvcnv  18934  grplmulf1o  18940  grpsubeq0  18952  grpsubadd  18954  grplactcnv  18969  isnsg4  19090  cycsubmel  19122  conjghm  19170  conjnmzb  19174  gacan  19217  gapm  19218  cntzrec  19248  oppgcntz  19279  fvcosymgeq  19345  odmulgeq  19473  dfod2  19480  sylow3lem3  19545  sylow3lem6  19548  lssnle  19590  lsmhash  19621  efgredlemb  19662  efgrelexlemb  19666  dprd2d2  19962  ablfac1eulem  19990  pgpfac1lem2  19993  pgpfac1lem4  19996  dvdsrval  20259  dvdsr02  20270  01eq0ring  20426  0ring01eqbi  20428  rngcinv  20529  ringcinv  20563  rmodislmodlem  20771  lvecinv  20960  rngqiprngimf1lem  21142  rspsn  21181  prmirredlem  21332  zndvds  21415  znleval  21420  psrbagconf1o  21799  psrbagconf1oOLD  21800  mplmonmul  21902  gsummoncoe1  22148  mat1dimelbas  22293  mat1dimbas  22294  1mavmul  22370  ma1repveval  22393  mulmarep1gsum1  22395  mdetunilem9  22442  m2cpminvid2lem  22576  pmatcollpw3lem  22605  mp2pm2mplem4  22631  toponsspwpw  22744  dmtopon  22745  cmpfi  23232  ssref  23336  qtopeu  23540  hmeoimaf1o  23594  txhmeo  23627  fbasrn  23708  rnelfmlem  23776  hauspwpwf1  23811  alexsubALTlem4  23874  qustgpopn  23944  qustgphaus  23947  fmucndlem  24116  isngp3  24427  isngp4  24441  metnrmlem1a  24694  icopnfcnv  24787  iccpnfcnv  24789  ivthle  25305  ivthle2  25306  dyadmbl  25449  mbfinf  25514  i1fmulclem  25552  itg1mulc  25554  mvth  25845  dvivth  25863  lhop2  25868  dvdsq1p  26016  reeff1o  26299  coseq1  26374  recosf1o  26384  resinf1o  26385  efopn  26506  cxpeq  26606  logreclem  26608  affineequiv  26669  affineequiv4  26672  affineequivne  26673  quad2  26685  dcubic  26692  mcubic  26693  quart  26707  atandm2  26723  rlimcnp2  26812  amgm  26836  wilthlem2  26914  mumullem2  27025  sqff1o  27027  dvdsflf1o  27032  gausslemma2dlem0i  27210  lgseisenlem2  27222  lgsquadlem2  27227  2lgslem1c  27239  2lgsoddprmlem2  27255  2lgsoddprm  27262  2sq2  27279  addsq2reu  27286  2sqreultlem  27293  2sqreunnltlem  27296  2sqreulem3  27299  sltval2  27502  sltintdifex  27507  sltres  27508  nosepon  27511  noextenddif  27514  nosepssdm  27532  nogt01o  27542  nosupprefixmo  27546  noinfprefixmo  27547  nosupno  27549  noinfno  27564  sleloe  27600  eqscut2  27652  scutbdaylt  27664  elold  27709  made0  27713  lrrecfr  27773  subadds  27891  renegscl  28106  tgjustf  28157  legtrid  28275  legso  28283  islmib  28471  lmicom  28472  lmiinv  28476  lmimid  28478  lmiopp  28486  colinearalglem2  28598  colinearalg  28601  ax5seglem4  28623  ax5seglem5  28624  axlowdimlem13  28645  axeuclidlem  28653  axeuclid  28654  axcontlem2  28656  axcontlem4  28658  elntg2  28676  structiedg0val  28715  usgredgsscusgredg  29149  fusgrn0degnn0  29189  umgr2v2evtxel  29212  vdiscusgrb  29220  uspgr2wlkeq  29336  wlk0prc  29344  wlklenvclwlk  29345  wlkp1lem8  29370  spthdep  29424  usgr2pthlem  29453  usgr2pth  29454  wlkiswwlksupgr2  29564  wlklnwwlkln2lem  29569  wwlksnextproplem3  29598  umgr2adedgwlk  29632  umgr2adedgspth  29635  umgr2wlkon  29637  umgrwwlks2on  29644  elwwlks2  29653  elwspths2spth  29654  clwlkclwwlklem2a4  29683  clwlkclwwlklem2  29686  erclwwlkref  29706  clwwlkf  29733  erclwwlknref  29755  erclwwlknsym  29756  erclwwlkntr  29757  hashecclwwlkn1  29763  umgrhashecclwwlk  29764  eupth2lem2  29905  eucrct2eupth  29931  numclwwlkqhash  30061  isgrpo  30183  hvsubaddi  30752  hire  30780  shmodsi  31075  omlsilem  31088  chcon1i  31151  chnlei  31171  pjoml3i  31272  cmbr2i  31282  chscllem2  31324  adjsym  31519  eigorthi  31523  dfadj2  31571  adjval2  31577  cnvadj  31578  dmadjrnb  31592  adjvalval  31623  cnlnadjeui  31763  cnlnssadj  31766  adjbdln  31769  pjimai  31862  pjin2i  31879  pjin3i  31880  stadd3i  31934  largei  31953  cvnbtwn3  31974  cvnbtwn4  31975  mddmd2  31995  superpos  32040  atnemeq0  32063  sumdmdii  32101  sumdmdlem  32104  addltmulALT  32132  opreu2reuALT  32150  foresf1o  32175  difeq  32189  disjrdx  32255  fcoinvbr  32269  fmptco1f1o  32290  dfimafnf  32293  funcnvmpt  32325  curry2ima  32363  intimafv  32365  cnvoprabOLD  32378  elicoelioo  32422  wrdt2ind  32550  swrdrn3  32552  orngsqr  32858  qusker  32900  eqg0el  32913  dvdsrspss  32931  lsmsnorb  32941  r1pid2  33120  algextdeglem8  33235  zarcls  33318  xrmulc1cn  33374  xrge0iifcnv  33377  ind1a  33481  esumfsup  33532  esumpcvgval  33540  esumcvg  33548  esum2dlem  33554  issgon  33585  eulerpartgbij  33835  eulerpartlemgh  33841  ballotlemsima  33978  bnj1366  34304  bnj553  34373  bnj964  34418  cusgredgex  34576  revwlk  34579  loop1cycl  34592  subfacp1lem3  34637  subfacp1lem5  34639  erdszelem9  34654  prv1n  34886  quad3  35119  br6  35197  elintfv  35206  dfon2lem5  35229  dfon2lem8  35232  brbigcup  35340  dfbigcup2  35341  elfix  35345  ellimits  35352  snelsingles  35364  dfiota3  35365  imageval  35372  brapply  35380  brsuccf  35383  funpartlem  35384  brfullfun  35390  dfrecs2  35392  dfrdg4  35393  altopthbg  35410  altopthc  35413  altopthd  35414  altopelaltxp  35418  brsegle  35550  outsideofrflx  35569  elicc3  35666  nn0prpw  35672  opnregcld  35679  cldregopn  35680  fneval  35701  topfneec  35704  knoppndvlem9  35860  bj-elgab  36283  bj-gabima  36284  bj-elsngl  36313  bj-snglc  36314  bj-projval  36341  bj-disj2r  36373  bj-restreg  36444  bj-0int  36446  copsex2b  36485  bj-inftyexpitaudisj  36550  bj-inftyexpidisj  36555  bj-bary1lem1  36656  topdifinffinlem  36692  topdifinfeq  36695  fvineqsnf1  36755  curf  36930  uncf  36931  curunc  36934  unccur  36935  poimirlem2  36954  poimirlem16  36968  poimirlem17  36969  poimirlem19  36971  poimirlem20  36972  poimirlem27  36979  mblfinlem2  36990  mbfresfi  36998  itg2addnclem2  37004  ftc1anclem3  37027  fdc  37077  heibor1  37142  opidonOLD  37184  0rngo  37359  smprngopr  37384  isfldidl  37400  isfldidl2  37401  eqbrb  37563  eqelb  37565  ideq2  37640  relcnveq  37655  n0elqs  37659  disjressuc2  37722  elrelscnveq  37826  disjdmqscossss  38137  lcvnbtwn3  38362  lcvexchlem1  38368  lsatnem0  38379  opcon1b  38532  omllaw2N  38578  cmtbr2N  38587  leatb  38626  cvlsupr2  38677  glbconxN  38713  islln3  38845  llnexatN  38856  islpln3  38868  lplnexatN  38898  islvol3  38911  dalem-cly  39006  isline4N  39112  2llnma3r  39123  poml4N  39288  4atex2  39412  4atex2-0bOLDN  39414  cdlemefrs29bpre0  39731  cdlemftr3  39900  cdlemb3  39941  cdlemg17h  40003  cdlemg17pq  40007  cdlemg19  40019  cdlemg21  40021  tendoex  40310  dva1dim  40320  dihglb2  40677  doch11  40708  dochsordN  40709  lcfrlem9  40885  hlhillcs  41297  lcmineqlem4  41364  metakunt1  41452  metakunt6  41457  metakunt15  41466  metakunt16  41467  fsuppind  41625  addsubeq4com  41655  elrfirn  41896  isnacs2  41907  isnacs3  41911  fiphp3d  42020  wopprc  42232  islnm2  42283  kercvrlsm  42288  fgraphopab  42415  tfsconcatlem  42549  tfsconcatrn  42555  tfsconcat0i  42558  tfsconcat0b  42559  tfsconcatrev  42561  oaun3lem1  42587  oadif1lem  42592  oadif1  42593  rp-fakeuninass  42730  snen1g  42738  iscard4  42747  sqrtcval  42855  frege124d  42975  frege129d  42977  frege92  43169  dffrege99  43176  clsk3nimkb  43254  clsk1indlem4  43258  clsk1indlem1  43259  ntrclsiso  43281  ntrclsk3  43284  ntrclsk13  43285  ntrneik4w  43314  extoimad  43379  int-sqdefd  43396  int-sqgeq0d  43401  radcnvrat  43536  bcc0  43562  opelopab4  43775  eqsbc2VD  44064  fzisoeu  44469  iuneqfzuz  44504  supxrleubrnmptf  44620  rexanuz2nf  44662  fsummulc1f  44746  fsumiunss  44750  fmul01lt1lem2  44760  sumnnodd  44805  fnlimfvre2  44852  limsupreuz  44912  limsupvaluz2  44913  liminfvalxr  44958  icccncfext  45062  cncfiooicc  45069  cncfioobdlem  45071  dvmptmulf  45112  dvmptfprodlem  45119  volioc  45147  itgioocnicc  45152  fourierdlem12  45294  fourierdlem20  45302  fourierdlem25  45307  fourierdlem33  45315  fourierdlem42  45324  fourierdlem52  45333  fourierdlem54  45335  fourierdlem57  45338  fourierdlem58  45339  fourierdlem59  45340  fourierdlem63  45344  fourierdlem65  45346  fourierdlem68  45349  fourierdlem73  45354  fourierdlem74  45355  fourierdlem75  45356  fourierdlem80  45361  fourierdlem81  45362  rrndistlt  45465  sge0ltfirpmpt2  45601  sge0pnfmpt  45620  hoidmv1le  45769  hoidmvle  45775  vonioolem2  45856  smflimlem3  45948  euabsneu  46197  funressnfv  46212  aiotaval  46262  reuf1odnf  46274  reuf1od  46275  afvpcfv0  46313  dfafn5a  46327  afvelrnb  46330  afvelrnb0  46331  dfaimafn2  46333  dfatsnafv2  46419  dfatdmfcoafv2  46421  f1oresf1o2  46458  0nelsetpreimafv  46517  fargshiftfo  46569  sprsymrelf1  46623  reupr  46649  fmtnorec2lem  46669  fmtnoprmfac1  46692  fmtnoprmfac2  46694  sfprmdvdsmersenne  46730  lighneallem2  46733  dfeven2  46776  dfodd3  46777  odd2np1ALTV  46801  even3prm2  46846  fppr2odd  46858  nnsum3primesgbe  46919  nnsum3primesle9  46921  isomuspgrlem2d  46958  0nodd  47007  2nodd  47009  lmod0rng  47066  rngcinvALTV  47113  ringcinvALTV  47147  lcoel0  47271  lindslinindimp2lem4  47304  ldepspr  47316  lincresunit3  47324  nn0sumshdiglemB  47468  nn0sumshdiglem1  47469  rrx2pnedifcoorneorr  47565  eenglngeehlnmlem1  47585  eenglngeehlnmlem2  47586  rrx2linest  47590  rrx2linest2  47592  rrxsphere  47596  line2ylem  47599  line2x  47602  itscnhlc0xyqsol  47613  itschlc0xyqsol1  47614  itsclinecirc0b  47622  2itscp  47629  inlinecirc02plem  47634