Theorem eqcom 2769

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

Syntax hints:   ↔ wb 208   = wceq 1560

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1800  df-cleq 2754

This theorem is referenced by:  eqcoms  2770  eqcomi  2771  neqcomd  2772  eqeq2d  2773  eqabcbw  2836  eqabcb  2902  necom  3010  nesym  3013  gencbvex  3510  clel5  3624  eqsbc2  3807  dfss  3923  sspsstri  4059  ssdifim  4225  disj4  4413  reuprg0  4661  preq1b  4804  invdisj  5086  disjprg  5096  dtruALT  5345  reusv3  5362  opthg2  5447  copsex2g  5462  copsex4g  5464  opcom  5470  opeqsng  5472  opeqpr  5474  snopeqop  5475  propeqop  5476  opthwiener  5483  vopelopabsb  5499  brab2d  5508  opthprc  5711  elxp3  5713  relop  5822  dmopab3  5895  rnopab3  5932  rncoeq  5958  restidsing  6042  somin1  6120  xpcan  6162  xpcan2  6163  dfrel4v  6176  dmsnn0  6194  reu3op  6279  reuop  6280  opreu2reurex  6281  ordtri2  6381  ordtri2or3  6448  suc11  6455  on0eqel  6471  snsn0non  6472  iota1  6500  iotan0  6511  sniota  6512  mptfnf  6656  fresaunres1  6737  dffn5  6925  fvelrnb  6927  dfimafn2  6930  funimass4  6931  feqmptdf  6937  fnsnfv  6946  dmfco  6963  funcnvmpt  6977  fndmdif  7023  fneqeql  7027  rexrn  7068  ralrn  7069  elrnrexdmb  7071  dffo4  7084  fssrescdmd  7108  funopsn  7130  funopsnOLD  7131  ftpg  7139  fprb  7178  ralima  7221  reximaOLD  7223  ralimaOLD  7224  fvclss  7225  dff13  7238  f1eqcocnv  7285  fnssintima  7346  imaeqsexvOLD  7347  riotaeqimp  7379  eusvobj2  7388  f1ocnvfv3  7391  oprabidw  7427  oprabid  7428  oprabv  7456  eloprabga  7505  ovelimab  7574  onmindif2  7790  br1steqg  7992  br2ndeqg  7993  dfoprab3  8035  opiota  8040  f1o2ndf1  8101  soseq  8139  brtpos2  8212  tpossym  8238  mpocurryd  8249  rdglim2  8403  tz7.48lem  8412  oaf1o  8532  omopthi  8631  erth2  8734  brecop  8792  erovlem  8795  ecopovsym  8801  eceqoveq  8804  xpcomco  9039  omxpenlem  9050  mapen  9113  nneneq  9174  unxpdomlem3  9202  unfilem1  9249  mapfien  9354  supgtoreq  9417  wemapsolem  9498  suc11reg  9574  inf3lem2  9584  inf3lem6  9588  ttrcltr  9671  djulf1o  9870  djurf1o  9871  infenaleph  10047  isinfcard  10048  dfac5  10085  cfeq0  10213  cfsuc  10214  ssfin4  10267  fin23lem25  10281  fin23lem22  10284  fin23lem40  10308  fin1a2lem5  10361  axcclem  10414  brdom7disj  10488  brdom6disj  10489  inar1  10733  psslinpr  10989  ltexprlem4  10997  ltsrpr  11035  mulgt0sr  11063  elreal  11089  ltresr  11098  leloe  11269  eqlei2  11294  addsubeq4  11445  subcan2  11456  negcon1  11483  negcon2  11484  addid0  11606  addeq0  11610  divmul2  11849  conjmul  11908  rereccl  11909  creur  12189  creui  12190  ind1a  12206  nndiv  12259  nn0sub  12531  elnn0z  12581  elznn0  12583  xrleloe  13146  ngtmnft  13169  icoshftf1o  13478  iccf1o  13500  fzen  13546  fzneuz  13613  injresinj  13797  fleqceilz  13864  mod0  13886  modmuladdnn0  13928  modirr  13955  addmodlteq  13959  nn0ennn  13992  hashrabsn01  14386  hashsdom  14394  hashgt12el2  14436  hashbclem  14465  hashfacen  14467  hashf1lem1  14468  hashtpg  14498  tpf1o  14514  fi1uzind  14520  ccatw2s1p1  14650  wrd2ind  14736  cshw1  14835  cshwsexa  14837  scshwfzeqfzo  14839  s2f1o  14929  wwlktovfo  14971  dmtrclfv  15031  cjreb  15150  leabs  15326  reusq0  15492  incexc2  15868  rpnnen2lem12  16257  dvdsval2  16289  dvdsabseq  16347  dvdsflip  16351  odd2np1  16375  oddm1even  16377  sqoddm1div8z  16388  m1exp1  16410  divalglem4  16430  divalglem8  16434  divalgb  16438  modremain  16442  zeqzmulgcd  16544  dfgcd2  16580  lcmfpr  16661  lcmftp  16670  lcmfunsnlem2  16674  divgcdcoprm0  16699  prm2orodd  16725  hashdvds  16810  oddprmdvds  16939  vdwlem12  17028  cshwshashlem1  17131  cshwsiun  17135  initoid  18034  termoid  18035  setcinv  18123  yonedainv  18313  joinfval  18403  joinfval2  18404  meetfval  18417  meetfval2  18418  latnle  18505  chnfi  18666  sgrp2nmndlem3  18962  grpid  19017  grpinvcnv  19048  grplmulf1o  19055  grpraddf1o  19056  grpsubeq0  19068  grpsubadd  19070  grplactcnv  19085  ressmulgnnd  19120  isnsg4  19208  eqg0el  19224  cycsubmel  19241  conjghm  19289  conjnmzb  19293  gacan  19345  gapm  19346  cntzrec  19376  oppgcntz  19404  fvcosymgeq  19469  odmulgeq  19597  dfod2  19604  sylow3lem3  19669  sylow3lem6  19672  lssnle  19714  lsmhash  19745  efgredlemb  19786  efgrelexlemb  19790  dprd2d2  20086  ablfac1eulem  20114  pgpfac1lem2  20117  pgpfac1lem4  20120  dvdsrval  20410  dvdsr02  20421  01eq0ring  20580  0ring01eqbi  20582  rngcinv  20687  ringcinv  20721  orngsqr  20915  rmodislmodlem  20996  lvecinv  21183  rngqiprngimf1lem  21364  rspsn  21403  prmirredlem  21524  zndvds  21601  znleval  21606  psrbagconf1o  21981  mplmonmul  22089  gsummoncoe1  22371  evl1maprhm  22442  mat1dimelbas  22531  mat1dimbas  22532  1mavmul  22608  ma1repveval  22631  mulmarep1gsum1  22633  mdetunilem9  22680  m2cpminvid2lem  22814  pmatcollpw3lem  22843  mp2pm2mplem4  22869  toponsspwpw  22982  dmtopon  22983  cmpfi  23468  ssref  23572  qtopeu  23776  hmeoimaf1o  23830  txhmeo  23863  fbasrn  23944  rnelfmlem  24012  hauspwpwf1  24047  alexsubALTlem4  24110  qustgpopn  24180  qustgphaus  24183  fmucndlem  24350  isngp3  24658  isngp4  24672  metnrmlem1a  24919  icopnfcnv  25004  iccpnfcnv  25006  ivthle  25518  ivthle2  25519  dyadmbl  25662  mbfinf  25727  i1fmulclem  25764  itg1mulc  25766  mvth  26054  dvivth  26072  lhop2  26077  r1pid2  26222  dvdsq1p  26223  reeff1o  26510  coseq1  26590  recosf1o  26600  resinf1o  26601  efopn  26723  cxpeq  26822  logreclem  26827  affineequiv  26888  affineequiv4  26891  affineequivne  26892  quad2  26904  dcubic  26911  mcubic  26912  quart  26926  atandm2  26942  rlimcnp2  27031  amgm  27055  wilthlem2  27133  mumullem2  27244  sqff1o  27246  dvdsflf1o  27251  gausslemma2dlem0i  27428  lgseisenlem2  27440  lgsquadlem2  27445  2lgslem1c  27457  2lgsoddprmlem2  27473  2lgsoddprm  27480  2sq2  27497  addsq2reu  27504  2sqreultlem  27511  2sqreunnltlem  27514  2sqreulem3  27517  ltsval2  27720  ltsintdifex  27725  ltsres  27726  nosepon  27729  noextenddif  27732  nosepssdm  27750  nogt01o  27760  nosupprefixmo  27764  noinfprefixmo  27765  nosupno  27767  noinfno  27782  lesloe  27818  eqcuts2  27879  cutbdaylt  27891  elold  27952  made0  27956  lrrecfr  28036  subadds  28163  oncutlt  28357  z12sge0  28576  renegscl  28591  tgjustf  28642  legtrid  28760  legso  28768  islmib  28960  lmicom  28961  lmiinv  28965  lmimid  28967  lmiopp  28975  prlngsym  29068  colinearalglem2  29108  colinearalg  29111  ax5seglem4  29133  ax5seglem5  29134  axlowdimlem13  29155  axeuclidlem  29163  axeuclid  29164  axcontlem2  29166  axcontlem4  29168  elntg2  29186  structiedg0val  29223  uspgredgiedg  29376  uspgriedgedg  29377  usgredgsscusgredg  29660  fusgrn0degnn0  29700  umgr2v2evtxel  29723  vdiscusgrb  29731  uspgr2wlkeq  29846  wlk0prc  29853  wlklenvclwlk  29854  wlkp1lem8  29879  spthdep  29934  usgr2pthlem  29963  usgr2pth  29964  wlkiswwlksupgr2  30077  wlklnwwlkln2lem  30082  wwlksnextproplem3  30111  umgr2adedgwlk  30145  umgr2adedgspth  30148  umgr2wlkon  30150  usgrwwlks2on  30158  umgrwwlks2on  30159  elwwlks2  30169  elwspths2spth  30170  clwlkclwwlklem2a4  30199  clwlkclwwlklem2  30202  erclwwlkref  30222  clwwlkf  30249  erclwwlknref  30271  erclwwlknsym  30272  erclwwlkntr  30273  hashecclwwlkn1  30279  umgrhashecclwwlk  30280  eupth2lem2  30421  eucrct2eupth  30447  numclwwlkqhash  30577  isgrpo  30700  hvsubaddi  31269  hire  31297  shmodsi  31592  omlsilem  31605  chcon1i  31668  chnlei  31688  pjoml3i  31789  cmbr2i  31799  chscllem2  31841  adjsym  32036  eigorthi  32040  dfadj2  32088  adjval2  32094  cnvadj  32095  dmadjrnb  32109  adjvalval  32140  cnlnadjeui  32280  cnlnssadj  32283  adjbdln  32286  pjimai  32379  pjin2i  32396  pjin3i  32397  stadd3i  32451  largei  32470  cvnbtwn3  32491  cvnbtwn4  32492  mddmd2  32512  superpos  32557  atnemeq0  32580  sumdmdii  32618  sumdmdlem  32621  addltmulALT  32649  opreu2reuALT  32676  foresf1o  32703  difeq  32717  disjrdx  32791  fcoinvbr  32805  fmptco1f1o  32835  dfimafnf  32838  curry2ima  32911  intimafv  32913  receqid  32946  elicoelioo  32980  fzo0opth  33005  wrdt2ind  33131  swrdrn3  33133  gsummptp1  33237  gsummulsubdishift1  33248  cntrval2  33351  domnprodeq0  33460  qusker  33535  dvdsrspss  33573  lsmsnorb  33577  1arithufdlem4  33743  r1pid2OLD  33805  selvply1rhmlemb  33816  psrmonmul  33847  esplyind  33872  algextdeglem8  34021  zarcls  34171  xrmulc1cn  34227  xrge0iifcnv  34230  esumfsup  34367  esumpcvgval  34375  esumcvg  34383  esum2dlem  34389  issgon  34420  eulerpartgbij  34669  eulerpartlemgh  34675  ballotlemsima  34813  bnj1366  35124  bnj553  35193  bnj964  35238  fineqvnttrclse  35420  cusgredgex  35472  revwlk  35475  loop1cycl  35487  subfacp1lem3  35532  subfacp1lem5  35534  erdszelem9  35549  prv1n  35781  ply1divalg3  35992  quad3  36020  br6  36107  elintfv  36115  dfon2lem5  36135  dfon2lem8  36138  brbigcup  36246  dfbigcup2  36247  elfix  36251  ellimits  36258  snelsingles  36270  dfiota3  36271  imageval  36278  brapply  36286  lemsuccf  36289  dfsuccf2  36291  funpartlem  36292  brfullfun  36298  dfrecs2  36300  dfrdg4  36301  altopthbg  36318  altopthc  36321  altopthd  36322  altopelaltxp  36326  brsegle  36458  outsideofrflx  36477  elicc3  36677  nn0prpw  36683  opnregcld  36690  cldregopn  36691  fneval  36712  topfneec  36715  knoppndvlem9  36958  bj-elgab  37424  bj-gabima  37425  bj-elsngl  37453  bj-snglc  37454  bj-projval  37481  bj-disj2r  37513  bj-restreg  37589  bj-0int  37591  copsex2gd  37630  copsex2b  37632  bj-inftyexpitaudisj  37697  bj-inftyexpidisj  37702  bj-bary1lem1  37803  topdifinffinlem  37841  topdifinfeq  37844  fvineqsnf1  37904  curf  38097  uncf  38098  curunc  38101  unccur  38102  poimirlem2  38121  poimirlem16  38135  poimirlem17  38136  poimirlem19  38138  poimirlem20  38139  poimirlem27  38146  mblfinlem2  38157  mbfresfi  38165  itg2addnclem2  38171  ftc1anclem3  38194  fdc  38244  heibor1  38309  opidonOLD  38351  0rngo  38526  smprngopr  38551  isfldidl  38567  isfldidl2  38568  eqbrb  38738  eqelb  38740  ideq2  38812  relcnveq  38827  n0elqs  38831  disjressuc2  38910  dfsucmap3  38962  dfsucmap4  38964  dmsucmap  38967  preuniqval  38995  elrelscnveq  39127  qseq  39232  disjdmqscossss  39405  lcvnbtwn3  39652  lcvexchlem1  39658  lsatnem0  39669  opcon1b  39822  omllaw2N  39868  cmtbr2N  39877  leatb  39916  cvlsupr2  39967  glbconxN  40002  islln3  40134  llnexatN  40145  islpln3  40157  lplnexatN  40187  islvol3  40200  dalem-cly  40295  isline4N  40401  2llnma3r  40412  poml4N  40577  4atex2  40701  4atex2-0bOLDN  40703  cdlemefrs29bpre0  41020  cdlemftr3  41189  cdlemb3  41230  cdlemg17h  41292  cdlemg17pq  41296  cdlemg19  41308  cdlemg21  41310  tendoex  41599  dva1dim  41609  dihglb2  41966  doch11  41997  dochsordN  41998  lcfrlem9  42174  hlhillcs  42582  lcmineqlem4  42649  aks6d1c7lem2  42798  aks5lem3a  42806  aks5lem6  42809  unitscyglem2  42813  unitscyglem3  42814  addsubeq4com  42889  ef11d  42948  redivmul2d  43055  fimgmcyclem  43151  fsuppind  43172  elrfirn  43276  isnacs2  43287  isnacs3  43291  fiphp3d  43396  wopprc  43607  islnm2  43655  kercvrlsm  43660  fgraphopab  43780  tfsconcatlem  43913  tfsconcatrn  43919  tfsconcat0i  43922  tfsconcat0b  43923  tfsconcatrev  43925  oaun3lem1  43951  oadif1lem  43956  oadif1  43957  rp-fakeuninass  44092  snen1g  44100  iscard4  44109  sqrtcval  44217  frege124d  44337  frege129d  44339  frege92  44531  dffrege99  44538  clsk3nimkb  44616  clsk1indlem4  44620  clsk1indlem1  44621  ntrclsiso  44643  ntrclsk3  44646  ntrclsk13  44647  ntrneik4w  44676  extoimad  44740  int-sqdefd  44757  int-sqgeq0d  44762  radcnvrat  44890  bcc0  44916  opelopab4  45127  eqsbc2VD  45415  fzisoeu  45879  iuneqfzuz  45911  supxrleubrnmptf  46025  rexanuz2nf  46066  fsummulc1f  46147  fsumiunss  46151  fmul01lt1lem2  46161  sumnnodd  46206  fnlimfvre2  46251  limsupreuz  46311  limsupvaluz2  46312  liminfvalxr  46357  icccncfext  46461  cncfiooicc  46468  cncfioobdlem  46470  dvmptmulf  46511  dvmptfprodlem  46518  volioc  46546  itgioocnicc  46551  fourierdlem12  46693  fourierdlem20  46701  fourierdlem25  46706  fourierdlem33  46714  fourierdlem42  46723  fourierdlem52  46732  fourierdlem54  46734  fourierdlem57  46737  fourierdlem58  46738  fourierdlem59  46739  fourierdlem63  46743  fourierdlem65  46745  fourierdlem68  46748  fourierdlem73  46753  fourierdlem74  46754  fourierdlem75  46755  fourierdlem80  46760  fourierdlem81  46761  rrndistlt  46864  sge0ltfirpmpt2  47000  sge0pnfmpt  47019  hoidmv1le  47168  hoidmvle  47174  vonioolem2  47255  smflimlem3  47347  chnsubseqwl  47455  cos5teq  47474  lambert0  47481  lamberte  47482  euabsneu  47622  funressnfv  47637  aiotaval  47689  reuf1odnf  47701  reuf1od  47702  afvpcfv0  47740  dfafn5a  47754  afvelrnb  47757  afvelrnb0  47758  dfaimafn2  47760  dfatsnafv2  47846  dfatdmfcoafv2  47848  f1oresf1o2  47885  ceilbi  47931  minusmodnep2tmod  47953  0nelsetpreimafv  47996  fargshiftfo  48048  sprsymrelf1  48102  reupr  48128  nprmmul1  48133  fmtnorec2lem  48151  fmtnoprmfac1  48174  fmtnoprmfac2  48176  sfprmdvdsmersenne  48212  lighneallem2  48215  dfeven2  48271  dfodd3  48272  odd2np1ALTV  48296  even3prm2  48341  fppr2odd  48353  nnsum3primesgbe  48414  nnsum3primesle9  48416  clnbgrsym  48460  dfvopnbgr2  48475  isuspgrim0  48516  isuspgrimlem  48517  dfgric2  48537  grtriprop  48563  uspgrlimlem3  48612  gpgvtxedg1  48686  pgnbgreunbgrlem2lem1  48736  pgnbgreunbgrlem2lem2  48737  0nodd  48792  2nodd  48794  lmod0rng  48851  rngcinvALTV  48898  ringcinvALTV  48932  lcoel0  49050  lindslinindimp2lem4  49083  ldepspr  49095  lincresunit3  49103  nn0sumshdiglemB  49242  nn0sumshdiglem1  49243  rrx2pnedifcoorneorr  49339  eenglngeehlnmlem1  49359  eenglngeehlnmlem2  49360  rrx2linest  49364  rrx2linest2  49366  rrxsphere  49370  line2ylem  49373  line2x  49376  itscnhlc0xyqsol  49387  itschlc0xyqsol1  49388  itsclinecirc0b  49396  2itscp  49403  inlinecirc02plem  49408  brab2dd  49449  uptr2  49842