Theorem eqcom 2768

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2753

This theorem is used by:  eqcoms  2769  eqcomi  2770  neqcomd  2771  eqeq2d  2772  eqabcbw  2835  eqabcb  2901  necom  3009  nesym  3012  gencbvex  3507  clel5  3619  eqsbc2  3802  dfss  3918  sspsstri  4054  ssdifim  4219  disj4  4412  reuprg0  4663  preq1b  4806  invdisj  5089  disjprg  5099  dtruALT  5350  reusv3  5367  opthg2  5448  copsex2g  5465  copsex4g  5467  opcom  5473  opeqsng  5475  opeqpr  5477  snopeqop  5478  propeqop  5479  opthwiener  5487  vopelopabsb  5503  brab2d  5512  opthprc  5715  elxp3  5717  relop  5828  dmopab3  5901  rnopab3  5938  rncoeq  5963  restidsing  6045  somin1  6127  xpcan  6168  xpcan2  6169  dfrel4v  6182  dmsnn0  6208  reu3op  6295  reuop  6296  opreu2reurex  6297  ordtri2  6398  ordtri2or3  6465  suc11  6472  on0eqel  6488  snsn0non  6489  iota1  6517  iotan0  6528  sniota  6529  mptfnf  6674  fresaunres1  6755  dffn5  6943  fvelrnb  6945  dfimafn2  6948  funimass4  6949  feqmptdf  6955  fnsnfv  6964  dmfco  6981  funcnvmpt  6995  fndmdif  7041  fneqeql  7045  rexrn  7087  ralrn  7088  elrnrexdmb  7090  dffo4  7103  fssrescdmd  7127  funopsn  7151  funopsnOLD  7152  ftpg  7160  fprb  7199  ralima  7243  fvclss  7245  dff13  7258  f1eqcocnv  7309  fnssintima  7372  riotaeqimp  7403  eusvobj2  7412  f1ocnvfv3  7415  oprabidw  7451  oprabid  7452  oprabv  7480  eloprabga  7529  ovelimab  7599  onmindif2  7821  br1steqg  8023  br2ndeqg  8024  dfoprab3  8065  opiota  8070  f1o2ndf1  8133  soseq  8176  brtpos2  8249  tpossym  8275  mpocurryd  8286  rdglim2  8440  tz7.48lemOLD  8451  oaf1o  8571  omopthi  8670  erth2  8773  brecop  8831  erovlem  8834  ecopovsym  8840  eceqoveq  8843  curf  8890  uncf  8891  xpcomco  9086  omxpenlem  9097  mapen  9160  nneneq  9221  unxpdomlem3  9249  unfilem1  9297  mapfien  9400  supgtoreq  9463  wemapsolem  9544  suc11reg  9620  inf3lem2  9630  inf3lem6  9634  ttrcltr  9717  djulf1o  9993  djurf1o  9994  infenaleph  10170  isinfcard  10171  dfac5  10207  cfeq0  10334  cfsuc  10335  ssfin4  10388  fin23lem25  10402  fin23lem22  10405  fin23lem40  10429  fin1a2lem5  10482  axcclem  10535  brdom7disj  10610  brdom6disj  10611  inar1  10860  psslinpr  11116  ltexprlem4  11124  ltsrpr  11162  mulgt0sr  11190  elreal  11216  ltresr  11225  leloe  11396  eqlei2  11421  addsubeq4  11572  subcan2  11583  negcon1  11610  negcon2  11611  addid0  11735  addeq0  11739  divmul2  11978  conjmul  12034  rereccl  12035  creur  12314  creui  12315  ind1a  12331  nndiv  12384  nn0sub  12656  elnn0z  12706  elznn0  12708  xrleloe  13273  ngtmnft  13296  icoshftf1o  13605  iccf1o  13627  fzen  13674  fzneuz  13742  injresinj  13926  fleqceilz  13994  mod0  14016  modmuladdnn0  14058  modirr  14085  addmodlteq  14089  nn0ennn  14122  hashrabsn01  14517  hashsdom  14525  hashgt12el2  14568  hashbclem  14597  hashfacen  14599  hashf1lem1  14600  hashtpg  14630  tpf1o  14646  fi1uzind  14652  ccatw2s1p1  14784  swrdrn3  14802  wrd2ind  14872  cshw1  14973  cshwsexa  14975  scshwfzeqfzo  14977  s2f1o  15067  wwlktovfo  15111  dmtrclfv  15171  cjreb  15290  leabs  15466  reusq0  15632  incexc2  16007  rpnnen2lem12  16393  dvdsval2  16425  dvdsabseq  16483  dvdsflip  16487  odd2np1  16511  oddm1even  16513  sqoddm1div8z  16524  m1exp1  16546  divalglem4  16566  divalglem8  16570  divalgb  16574  modremain  16578  zeqzmulgcd  16682  dfgcd2  16719  lcmfpr  16802  lcmftp  16811  lcmfunsnlem2  16815  divgcdcoprm0  16840  prm2orodd  16866  hashdvds  16952  oddprmdvds  17081  vdwlem12  17170  cshwshashlem1  17273  cshwsiun  17277  initoid  18176  termoid  18177  setcinv  18265  yonedainv  18455  joinfval  18545  joinfval2  18546  meetfval  18559  meetfval2  18560  latnle  18647  chnfi  18808  mgmidpfod  18857  sgrp2nmndlem3  19124  grpid  19186  grpinvcnv  19217  grplmulf1o  19223  grpraddf1o  19224  grpsubeq0  19236  grpsubadd  19238  grplactcnv  19253  ressmulgnnd  19288  isnsg4  19377  eqg0el  19398  cycsubmel  19415  conjghm  19463  conjnmzb  19467  gacan  19519  gapm  19520  cntzrec  19550  oppgcntz  19578  fvcosymgeq  19643  odmulgeq  19771  dfod2  19778  sylow3lem3  19843  sylow3lem6  19846  lssnle  19888  lsmhash  19919  efgredlemb  19960  efgrelexlemb  19964  dprd2d2  20260  ablfac1eulem  20288  pgpfac1lem2  20291  pgpfac1lem4  20294  dvdsrval  20591  dvdsr02  20602  01eq0ring  20781  0ring01eqbi2  20783  0ring01eqbi  20784  rngcinv  20889  ringcinv  20923  orngsqr  21123  rmodislmodlem  21204  lvecinv  21391  isfieldidl2  21541  rngqiprngimf1lem  21590  rspsn  21657  prmirredlem  21778  zndvds  21855  znleval  21860  psrbagconf1o  22237  mplmonmul  22345  gsummoncoe1  22626  evl1maprhm  22697  mat1dimelbas  22786  mat1dimbas  22787  1mavmul  22863  ma1repveval  22886  mulmarep1gsum1  22888  mdetunilem9  22935  m2cpminvid2lem  23072  pmatcollpw3lem  23101  mp2pm2mplem4  23127  toponsspwpw  23240  dmtopon  23241  cmpfi  23726  ssref  23831  qtopeu  24035  hmeoimaf1o  24089  txhmeo  24122  fbasrn  24203  rnelfmlem  24271  hauspwpwf1  24306  alexsubALTlem4  24369  qustgpopn  24439  qustgphaus  24442  fmucndlem  24609  isngp3  24917  isngp4  24931  metnrmlem1a  25178  icopnfcnv  25263  iccpnfcnv  25265  ivthle  25777  ivthle2  25778  dyadmbl  25921  mbfinf  25986  i1fmulclem  26023  itg1mulc  26025  mvth  26312  dvivth  26330  lhop2  26335  r1pid2  26480  dvdsq1p  26481  plyconz  26631  reeff1o  26774  coseq1  26853  recosf1o  26863  resinf1o  26864  efopn  26986  cxpeq  27085  logreclem  27090  affineequiv  27151  affineequiv4  27154  affineequivne  27155  quad2  27167  dcubic  27174  mcubic  27175  quart  27189  atandm2  27205  rlimcnp2  27294  amgm  27318  wilthlem2  27396  mumullem2  27507  sqff1o  27509  dvdsflf1o  27514  gausslemma2dlem0i  27691  lgseisenlem2  27703  lgsquadlem2  27708  2lgslem1c  27720  2lgsoddprmlem2  27736  2lgsoddprm  27743  2sq2  27760  addsq2reu  27767  2sqreultlem  27774  2sqreunnltlem  27777  2sqreulem3  27780  ltsval2  28013  ltsintdifex  28018  ltsres  28019  nosepon  28022  noextenddif  28025  nosepssdm  28043  nogt01o  28053  nosupprefixmo  28057  noinfprefixmo  28058  nosupno  28060  noinfno  28075  lesloe  28111  eqcuts2  28172  cutbdaylt  28184  elold  28245  made0  28249  lrrecfr  28329  subadds  28456  oncutlt  28650  z12sge0  28869  renegscl  28884  tgjustf  28935  legtrid  29054  legso  29062  islmib  29292  lmicom  29293  lmiinv  29297  lmimid  29299  lmiopp  29308  prlngsym  29419  colinearalglem2  29485  colinearalg  29488  ax5seglem4  29510  ax5seglem5  29511  axlowdimlem13  29532  axeuclidlem  29540  axeuclid  29541  axcontlem2  29543  axcontlem4  29545  elntg2  29563  structiedg0val  29600  uspgredgiedg  29756  uspgriedgedg  29757  usgredgsscusgredg  30040  fusgrn0degnn0  30080  umgr2v2evtxel  30103  vdiscusgrb  30111  uspgr2wlkeq  30226  wlk0prc  30233  wlklenvclwlk  30234  wlkp1lem8  30259  revwlk  30267  spthdep  30320  usgr2pthlem  30349  usgr2pth  30350  wlkiswwlksupgr2  30466  wlklnwwlkln2lem  30471  wwlksnextproplem3  30500  umgr2adedgwlk  30534  umgr2adedgspth  30537  umgr2wlkon  30539  usgrwwlks2on  30547  umgrwwlks2on  30548  elwwlks2  30558  elwspths2spth  30559  clwlkclwwlklem2a4  30588  clwlkclwwlklem2  30591  erclwwlkref  30611  clwwlkf  30638  erclwwlknref  30660  erclwwlknsym  30661  erclwwlkntr  30662  hashecclwwlkn1  30668  umgrhashecclwwlk  30669  loop1cycl  30744  eupth2lem2  30820  eucrct2eupth  30846  numclwwlkqhash  30976  isgrpo  31099  hvsubaddi  31668  hire  31696  shmodsi  31991  omlsilem  32004  chcon1i  32067  chnlei  32087  pjoml3i  32188  cmbr2i  32198  chscllem2  32240  adjsym  32435  eigorthi  32439  dfadj2  32487  adjval2  32493  cnvadj  32494  dmadjrnb  32508  adjvalval  32539  cnlnadjeui  32679  cnlnssadj  32682  adjbdln  32685  pjimai  32778  pjin2i  32795  pjin3i  32796  stadd3i  32850  largei  32869  cvnbtwn3  32890  cvnbtwn4  32891  mddmd2  32911  superpos  32956  atnemeq0  32979  sumdmdii  33017  sumdmdlem  33020  addltmulALT  33048  opreu2reuALT  33073  foresf1o  33100  difeq  33114  disjrdx  33185  fcoinvbr  33199  fmptco1f1o  33227  dfimafnf  33230  curry2ima  33302  intimafv  33304  receqid  33336  elicoelioo  33370  fzo0opth  33395  wrdt2ind  33516  gsummptp1  33618  gsummulsubdishift1  33629  cntrval2  33732  domnprodeq0  33840  qusker  33910  dvdsrspss  33942  lsmsnorb  33946  1arithufdlem4  34079  selvply1rhmlemb  34151  psrmonmul  34182  esplyind  34207  algextdeglem8  34356  zarcls  34506  xrmulc1cn  34562  xrge0iifcnv  34565  esumfsup  34702  esumpcvgval  34710  esumcvg  34718  esum2dlem  34724  issgon  34755  eulerpartgbij  35004  eulerpartlemgh  35010  ballotlemsima  35148  bnj1366  35459  bnj553  35528  bnj964  35573  dfscott3  35743  fineqvnttrclse  35792  cusgredgex  35906  subfacp1lem3  35947  subfacp1lem5  35949  erdszelem9  35964  prv1n  36196  ply1divalg3  36407  quad3  36435  br6  36522  elintfv  36530  dfon2lem5  36549  dfon2lem8  36552  brbigcup  36660  dfbigcup2  36661  elfix  36665  ellimits  36672  snelsingles  36684  dfiota3  36685  imageval  36692  brapply  36700  lemsuccf  36703  dfsuccf2  36705  funpartlem  36706  brfullfun  36712  dfrecs2  36714  dfrdg4  36715  altopthbg  36733  altopthc  36736  altopthd  36737  altopelaltxp  36741  brsegle  36873  outsideofrflx  36892  elicc3  37105  nn0prpw  37111  opnregcld  37118  cldregopn  37119  fneval  37140  topfneec  37143  knoppndvlem9  37386  bj-elgab  37852  bj-gabima  37853  bj-elsngl  37881  bj-snglc  37882  bj-projval  37909  bj-disj2r  37941  bj-restreg  38020  bj-0int  38022  copsex2gd  38059  copsex2b  38061  bj-inftyexpitaudisj  38126  bj-inftyexpidisj  38131  bj-bary1lem1  38232  topdifinffinlem  38270  topdifinfeq  38273  fvineqsnf1  38333  curunc  38525  unccur  38526  poimirlem2  38540  poimirlem16  38554  poimirlem17  38555  poimirlem19  38557  poimirlem20  38558  poimirlem27  38565  mblfinlem2  38576  mbfresfi  38584  itg2addnclem2  38590  ftc1anclem3  38613  findcard4  38632  fdc  38679  heibor1  38744  opidonOLD  38786  0rngo  38961  smprngopr  38986  isfldidl  39002  isfldidl2  39003  eqbrb  39171  eqelb  39173  ideq2  39245  relcnveq  39260  n0elqs  39264  disjressuc2  39343  dfsucmap3  39395  dfsucmap4  39397  dmsucmap  39400  preuniqval  39428  elrelscnveq  39560  qseq  39665  disjdmqscossss  39838  lcvnbtwn3  40085  lcvexchlem1  40091  lsatnem0  40102  opcon1b  40255  omllaw2N  40301  cmtbr2N  40310  leatb  40349  cvlsupr2  40400  glbconxN  40435  islln3  40567  llnexatN  40578  islpln3  40590  lplnexatN  40620  islvol3  40633  dalem-cly  40728  isline4N  40834  2llnma3r  40845  poml4N  41010  4atex2  41134  4atex2-0bOLDN  41136  cdlemefrs29bpre0  41453  cdlemftr3  41622  cdlemb3  41663  cdlemg17h  41725  cdlemg17pq  41729  cdlemg19  41741  cdlemg21  41743  tendoex  42032  dva1dim  42042  dihglb2  42399  doch11  42430  dochsordN  42431  lcfrlem9  42607  hlhillcs  43015  lcmineqlem4  43082  aks6d1c7lem2  43231  aks5lem3a  43239  aks5lem6  43242  unitscyglem2  43246  unitscyglem3  43247  addsubeq4com  43337  ef11d  43390  redivmul2d  43497  fimgmcyclem  43597  fsuppind  43618  elrfirn  43705  isnacs2  43716  isnacs3  43720  fiphp3d  43825  wopprc  44036  islnm2  44079  kercvrlsm  44084  fgraphopab  44204  tfsconcatlem  44337  tfsconcatrn  44343  tfsconcat0i  44346  tfsconcat0b  44347  tfsconcatrev  44349  oaun3lem1  44375  oadif1lem  44380  oadif1  44381  rp-fakeuninass  44516  snen1g  44524  iscard4  44533  sqrtcval  44640  frege124d  44760  frege129d  44762  frege92  44954  dffrege99  44961  clsk3nimkb  45039  clsk1indlem4  45043  clsk1indlem1  45044  ntrclsiso  45066  ntrclsk3  45069  ntrclsk13  45070  ntrneik4w  45099  extoimad  45163  int-sqdefd  45180  int-sqgeq0d  45185  radcnvrat  45297  bcc0  45323  opelopab4  45533  eqsbc2VD  45821  fzisoeu  46315  iuneqfzuz  46346  supxrleubrnmptf  46460  rexanuz2nf  46501  fsummulc1f  46582  fsumiunss  46586  fmul01lt1lem2  46596  sumnnodd  46641  fnlimfvre2  46686  limsupreuz  46746  limsupvaluz2  46747  liminfvalxr  46792  icccncfext  46896  cncfiooicc  46903  cncfioobdlem  46905  dvmptmulf  46946  dvmptfprodlem  46953  volioc  46981  itgioocnicc  46986  fourierdlem12  47128  fourierdlem20  47136  fourierdlem25  47141  fourierdlem33  47149  fourierdlem42  47158  fourierdlem52  47167  fourierdlem54  47169  fourierdlem57  47172  fourierdlem58  47173  fourierdlem59  47174  fourierdlem63  47178  fourierdlem65  47180  fourierdlem68  47183  fourierdlem73  47188  fourierdlem74  47189  fourierdlem75  47190  fourierdlem80  47195  fourierdlem81  47196  rrndistlt  47299  sge0ltfirpmpt2  47435  sge0pnfmpt  47454  hoidmv1le  47603  hoidmvle  47609  vonioolem2  47690  smflimlem3  47782  chnsubseqwl  47888  cos5teq  47925  lambert0  47936  lamberte  47937  euabsneu  48097  funressnfv  48112  aiotaval  48164  reuf1odnf  48176  reuf1od  48177  afvpcfv0  48215  dfafn5a  48229  afvelrnb  48232  afvelrnb0  48233  dfaimafn2  48235  dfatsnafv2  48321  dfatdmfcoafv2  48323  f1oresf1o2  48360  ceilbi  48406  minusmodnep2tmod  48428  0nelsetpreimafv  48471  fargshiftfo  48523  sprsymrelf1  48577  reupr  48603  nprmmul1  48608  fmtnorec2lem  48626  fmtnoprmfac1  48649  fmtnoprmfac2  48651  sfprmdvdsmersenne  48687  lighneallem2  48690  dfeven2  48746  dfodd3  48747  odd2np1ALTV  48771  even3prm2  48816  fppr2odd  48828  nnsum3primesgbe  48889  nnsum3primesle9  48891  clnbgrsym  48935  dfvopnbgr2  48950  isuspgrim0  48991  isuspgrimlem  48992  dfgric2  49012  grtriprop  49038  uspgrlimlem3  49087  gpgvtxedg1  49161  pgnbgreunbgrlem2lem1  49211  pgnbgreunbgrlem2lem2  49212  0nodd  49266  2nodd  49268  lmod0rng  49325  rngcinvALTV  49372  ringcinvALTV  49406  isidom3  49441  lcoel0  49539  lindslinindimp2lem4  49572  ldepspr  49584  lincresunit3  49592  nn0sumshdiglemB  49731  nn0sumshdiglem1  49732  rrx2pnedifcoorneorr  49828  eenglngeehlnmlem1  49848  eenglngeehlnmlem2  49849  rrx2linest  49853  rrx2linest2  49855  rrxsphere  49859  line2ylem  49862  line2x  49865  itscnhlc0xyqsol  49876  itschlc0xyqsol1  49877  itsclinecirc0b  49885  2itscp  49892  inlinecirc02plem  49897  brab2dd  49937  uptr2  50328