Theorem eqcom 2743

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

Syntax hints:   ↔ wb 206   = wceq 1541

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 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2728

This theorem is referenced by:  eqcoms  2744  eqcomi  2745  neqcomd  2746  eqeq2d  2747  eqabcbw  2810  eqabcb  2876  necom  2985  nesym  2988  gencbvex  3499  clel5  3619  eqsbc2  3804  dfss  3920  sspsstri  4057  ssnelpss  4066  ssdifim  4225  disj4  4411  reuprg0  4659  preq1b  4802  invdisj  5084  disjprg  5094  dtruALT  5333  reusv3  5350  opthg2  5427  copsex2g  5441  copsex4g  5443  opcom  5449  opeqsng  5451  opeqpr  5453  snopeqop  5454  propeqop  5455  opthwiener  5462  vopelopabsb  5477  opthprc  5688  elxp3  5690  relop  5799  dmopab3  5868  rnopab3  5905  rncoeq  5931  restidsing  6012  somin1  6090  xpcan  6134  xpcan2  6135  dfrel4v  6148  dmsnn0  6165  reu3op  6250  reuop  6251  opreu2reurex  6252  ordtri2  6352  ordtri2or3  6419  suc11  6426  on0eqel  6442  snsn0non  6443  iota1  6471  iotan0  6482  sniota  6483  mptfnf  6627  fresaunres1  6707  dffn5  6892  fvelrnb  6894  dfimafn2  6897  funimass4  6898  feqmptdf  6904  fnsnfv  6913  dmfco  6930  fndmdif  6987  fneqeql  6991  rexrn  7032  ralrn  7033  elrnrexdmb  7035  dffo4  7048  fssrescdmd  7071  funopsn  7093  ftpg  7101  fprb  7140  ralima  7183  reximaOLD  7185  ralimaOLD  7186  fvclss  7187  dff13  7200  f1eqcocnv  7247  fnssintima  7308  imaeqsexvOLD  7309  riotaeqimp  7341  eusvobj2  7350  f1ocnvfv3  7353  oprabidw  7389  oprabid  7390  oprabv  7418  eloprabga  7467  ovelimab  7536  onmindif2  7752  br1steqg  7955  br2ndeqg  7956  dfoprab3  7998  opiota  8003  f1o2ndf1  8064  soseq  8101  brtpos2  8174  tpossym  8200  mpocurryd  8211  rdglim2  8363  tz7.48lem  8372  oaf1o  8490  omopthi  8589  erth2  8690  brecop  8747  erovlem  8750  ecopovsym  8756  eceqoveq  8759  xpcomco  8995  omxpenlem  9006  mapen  9069  nneneq  9130  unxpdomlem3  9158  unfilem1  9205  mapfien  9311  supgtoreq  9374  wemapsolem  9455  suc11reg  9528  inf3lem2  9538  inf3lem6  9542  ttrcltr  9625  djulf1o  9824  djurf1o  9825  infenaleph  10001  isinfcard  10002  dfac5  10039  cfeq0  10166  cfsuc  10167  ssfin4  10220  fin23lem25  10234  fin23lem22  10237  fin23lem40  10261  fin1a2lem5  10314  axcclem  10367  brdom7disj  10441  brdom6disj  10442  inar1  10686  psslinpr  10942  ltexprlem4  10950  ltsrpr  10988  mulgt0sr  11016  elreal  11042  ltresr  11051  leloe  11219  eqlei2  11244  addsubeq4  11395  subcan2  11406  negcon1  11433  negcon2  11434  addid0  11556  addeq0  11560  divmul2  11800  conjmul  11858  rereccl  11859  creur  12139  creui  12140  nndiv  12191  nn0sub  12451  elnn0z  12501  elznn0  12503  xrleloe  13058  ngtmnft  13081  icoshftf1o  13390  iccf1o  13412  fzen  13457  fzneuz  13524  injresinj  13707  fleqceilz  13774  mod0  13796  modmuladdnn0  13838  modirr  13865  addmodlteq  13869  nn0ennn  13902  hashrabsn01  14296  hashsdom  14304  hashgt12el2  14346  hashbclem  14375  hashfacen  14377  hashf1lem1  14378  hashtpg  14408  tpf1o  14424  fi1uzind  14430  ccatw2s1p1  14560  wrd2ind  14646  cshw1  14745  cshwsexa  14747  scshwfzeqfzo  14749  s2f1o  14839  wwlktovfo  14881  dmtrclfv  14941  cjreb  15046  leabs  15222  reusq0  15388  incexc2  15761  rpnnen2lem12  16150  dvdsval2  16182  dvdsabseq  16240  dvdsflip  16244  odd2np1  16268  oddm1even  16270  sqoddm1div8z  16281  m1exp1  16303  divalglem4  16323  divalglem8  16327  divalgb  16331  modremain  16335  zeqzmulgcd  16437  dfgcd2  16473  lcmfpr  16554  lcmftp  16563  lcmfunsnlem2  16567  divgcdcoprm0  16592  prm2orodd  16618  hashdvds  16702  oddprmdvds  16831  vdwlem12  16920  cshwshashlem1  17023  cshwsiun  17027  initoid  17925  termoid  17926  setcinv  18014  yonedainv  18204  joinfval  18294  joinfval2  18295  meetfval  18308  meetfval2  18309  latnle  18396  chnfi  18557  sgrp2nmndlem3  18850  grpid  18905  grpinvcnv  18936  grplmulf1o  18943  grpraddf1o  18944  grpsubeq0  18956  grpsubadd  18958  grplactcnv  18973  ressmulgnnd  19008  isnsg4  19096  eqg0el  19112  cycsubmel  19129  conjghm  19178  conjnmzb  19182  gacan  19234  gapm  19235  cntzrec  19265  oppgcntz  19293  fvcosymgeq  19358  odmulgeq  19486  dfod2  19493  sylow3lem3  19558  sylow3lem6  19561  lssnle  19603  lsmhash  19634  efgredlemb  19675  efgrelexlemb  19679  dprd2d2  19975  ablfac1eulem  20003  pgpfac1lem2  20006  pgpfac1lem4  20009  dvdsrval  20297  dvdsr02  20308  01eq0ring  20463  0ring01eqbi  20465  rngcinv  20570  ringcinv  20604  orngsqr  20799  rmodislmodlem  20880  lvecinv  21068  rngqiprngimf1lem  21249  rspsn  21288  dfcnfldOLD  21325  prmirredlem  21427  zndvds  21504  znleval  21509  psrbagconf1o  21885  mplmonmul  21991  gsummoncoe1  22252  evl1maprhm  22323  mat1dimelbas  22415  mat1dimbas  22416  1mavmul  22492  ma1repveval  22515  mulmarep1gsum1  22517  mdetunilem9  22564  m2cpminvid2lem  22698  pmatcollpw3lem  22727  mp2pm2mplem4  22753  toponsspwpw  22866  dmtopon  22867  cmpfi  23352  ssref  23456  qtopeu  23660  hmeoimaf1o  23714  txhmeo  23747  fbasrn  23828  rnelfmlem  23896  hauspwpwf1  23931  alexsubALTlem4  23994  qustgpopn  24064  qustgphaus  24067  fmucndlem  24234  isngp3  24542  isngp4  24556  metnrmlem1a  24803  icopnfcnv  24896  iccpnfcnv  24898  ivthle  25413  ivthle2  25414  dyadmbl  25557  mbfinf  25622  i1fmulclem  25659  itg1mulc  25661  mvth  25953  dvivth  25971  lhop2  25976  r1pid2  26123  dvdsq1p  26124  reeff1o  26413  coseq1  26490  recosf1o  26500  resinf1o  26501  efopn  26623  cxpeq  26723  logreclem  26728  affineequiv  26789  affineequiv4  26792  affineequivne  26793  quad2  26805  dcubic  26812  mcubic  26813  quart  26827  atandm2  26843  rlimcnp2  26932  amgm  26957  wilthlem2  27035  mumullem2  27146  sqff1o  27148  dvdsflf1o  27153  gausslemma2dlem0i  27331  lgseisenlem2  27343  lgsquadlem2  27348  2lgslem1c  27360  2lgsoddprmlem2  27376  2lgsoddprm  27383  2sq2  27400  addsq2reu  27407  2sqreultlem  27414  2sqreunnltlem  27417  2sqreulem3  27420  ltsval2  27624  ltsintdifex  27629  ltsres  27630  nosepon  27633  noextenddif  27636  nosepssdm  27654  nogt01o  27664  nosupprefixmo  27668  noinfprefixmo  27669  nosupno  27671  noinfno  27686  lesloe  27722  eqcuts2  27782  cutbdaylt  27794  elold  27855  made0  27859  lrrecfr  27939  subadds  28066  oncutlt  28260  z12sge0  28479  renegscl  28494  tgjustf  28545  legtrid  28663  legso  28671  islmib  28859  lmicom  28860  lmiinv  28864  lmimid  28866  lmiopp  28874  colinearalglem2  28980  colinearalg  28983  ax5seglem4  29005  ax5seglem5  29006  axlowdimlem13  29027  axeuclidlem  29035  axeuclid  29036  axcontlem2  29038  axcontlem4  29040  elntg2  29058  structiedg0val  29095  uspgredgiedg  29248  uspgriedgedg  29249  usgredgsscusgredg  29533  fusgrn0degnn0  29573  umgr2v2evtxel  29596  vdiscusgrb  29604  uspgr2wlkeq  29719  wlk0prc  29726  wlklenvclwlk  29727  wlkp1lem8  29752  spthdep  29807  usgr2pthlem  29836  usgr2pth  29837  wlkiswwlksupgr2  29950  wlklnwwlkln2lem  29955  wwlksnextproplem3  29984  umgr2adedgwlk  30018  umgr2adedgspth  30021  umgr2wlkon  30023  usgrwwlks2on  30031  umgrwwlks2on  30032  elwwlks2  30042  elwspths2spth  30043  clwlkclwwlklem2a4  30072  clwlkclwwlklem2  30075  erclwwlkref  30095  clwwlkf  30122  erclwwlknref  30144  erclwwlknsym  30145  erclwwlkntr  30146  hashecclwwlkn1  30152  umgrhashecclwwlk  30153  eupth2lem2  30294  eucrct2eupth  30320  numclwwlkqhash  30450  isgrpo  30572  hvsubaddi  31141  hire  31169  shmodsi  31464  omlsilem  31477  chcon1i  31540  chnlei  31560  pjoml3i  31661  cmbr2i  31671  chscllem2  31713  adjsym  31908  eigorthi  31912  dfadj2  31960  adjval2  31966  cnvadj  31967  dmadjrnb  31981  adjvalval  32012  cnlnadjeui  32152  cnlnssadj  32155  adjbdln  32158  pjimai  32251  pjin2i  32268  pjin3i  32269  stadd3i  32323  largei  32342  cvnbtwn3  32363  cvnbtwn4  32364  mddmd2  32384  superpos  32429  atnemeq0  32452  sumdmdii  32490  sumdmdlem  32493  addltmulALT  32521  opreu2reuALT  32551  foresf1o  32579  difeq  32593  disjrdx  32666  fcoinvbr  32680  brab2d  32683  fmptco1f1o  32711  dfimafnf  32714  funcnvmpt  32745  curry2ima  32788  intimafv  32790  receqid  32824  elicoelioo  32858  fzo0opth  32883  ind1a  32938  wrdt2ind  33035  swrdrn3  33037  gsummptp1  33140  gsummulsubdishift1  33151  cntrval2  33253  domnprodeq0  33358  qusker  33430  dvdsrspss  33468  lsmsnorb  33472  1arithufdlem4  33628  r1pid2OLD  33690  esplyind  33731  algextdeglem8  33881  zarcls  34031  xrmulc1cn  34087  xrge0iifcnv  34090  esumfsup  34227  esumpcvgval  34235  esumcvg  34243  esum2dlem  34249  issgon  34280  eulerpartgbij  34529  eulerpartlemgh  34535  ballotlemsima  34673  bnj1366  34985  bnj553  35054  bnj964  35099  fineqvnttrclse  35280  cusgredgex  35316  revwlk  35319  loop1cycl  35331  subfacp1lem3  35376  subfacp1lem5  35378  erdszelem9  35393  prv1n  35625  ply1divalg3  35836  quad3  35864  br6  35951  elintfv  35959  dfon2lem5  35979  dfon2lem8  35982  brbigcup  36090  dfbigcup2  36091  elfix  36095  ellimits  36102  snelsingles  36114  dfiota3  36115  imageval  36122  brapply  36130  lemsuccf  36133  dfsuccf2  36135  funpartlem  36136  brfullfun  36142  dfrecs2  36144  dfrdg4  36145  altopthbg  36162  altopthc  36165  altopthd  36166  altopelaltxp  36170  brsegle  36302  outsideofrflx  36321  elicc3  36511  nn0prpw  36517  opnregcld  36524  cldregopn  36525  fneval  36546  topfneec  36549  knoppndvlem9  36720  bj-elgab  37140  bj-gabima  37141  bj-elsngl  37169  bj-snglc  37170  bj-projval  37197  bj-disj2r  37229  bj-restreg  37304  bj-0int  37306  copsex2b  37345  bj-inftyexpitaudisj  37410  bj-inftyexpidisj  37415  bj-bary1lem1  37516  topdifinffinlem  37552  topdifinfeq  37555  fvineqsnf1  37615  curf  37799  uncf  37800  curunc  37803  unccur  37804  poimirlem2  37823  poimirlem16  37837  poimirlem17  37838  poimirlem19  37840  poimirlem20  37841  poimirlem27  37848  mblfinlem2  37859  mbfresfi  37867  itg2addnclem2  37873  ftc1anclem3  37896  fdc  37946  heibor1  38011  opidonOLD  38053  0rngo  38228  smprngopr  38253  isfldidl  38269  isfldidl2  38270  eqbrb  38435  eqelb  38437  ideq2  38506  relcnveq  38521  n0elqs  38525  disjressuc2  38596  dfsucmap3  38637  dfsucmap4  38639  dmsucmap  38642  preuniqval  38669  elrelscnveq  38801  qseq  38907  disjdmqscossss  39062  lcvnbtwn3  39288  lcvexchlem1  39294  lsatnem0  39305  opcon1b  39458  omllaw2N  39504  cmtbr2N  39513  leatb  39552  cvlsupr2  39603  glbconxN  39638  islln3  39770  llnexatN  39781  islpln3  39793  lplnexatN  39823  islvol3  39836  dalem-cly  39931  isline4N  40037  2llnma3r  40048  poml4N  40213  4atex2  40337  4atex2-0bOLDN  40339  cdlemefrs29bpre0  40656  cdlemftr3  40825  cdlemb3  40866  cdlemg17h  40928  cdlemg17pq  40932  cdlemg19  40944  cdlemg21  40946  tendoex  41235  dva1dim  41245  dihglb2  41602  doch11  41633  dochsordN  41634  lcfrlem9  41810  hlhillcs  42218  lcmineqlem4  42286  aks6d1c7lem2  42435  aks5lem3a  42443  aks5lem6  42446  unitscyglem2  42450  unitscyglem3  42451  addsubeq4com  42535  ef11d  42594  fimgmcyclem  42788  fsuppind  42833  elrfirn  42937  isnacs2  42948  isnacs3  42952  fiphp3d  43061  wopprc  43272  islnm2  43320  kercvrlsm  43325  fgraphopab  43445  tfsconcatlem  43578  tfsconcatrn  43584  tfsconcat0i  43587  tfsconcat0b  43588  tfsconcatrev  43590  oaun3lem1  43616  oadif1lem  43621  oadif1  43622  rp-fakeuninass  43757  snen1g  43765  iscard4  43774  sqrtcval  43882  frege124d  44002  frege129d  44004  frege92  44196  dffrege99  44203  clsk3nimkb  44281  clsk1indlem4  44285  clsk1indlem1  44286  ntrclsiso  44308  ntrclsk3  44311  ntrclsk13  44312  ntrneik4w  44341  extoimad  44405  int-sqdefd  44422  int-sqgeq0d  44427  radcnvrat  44555  bcc0  44581  opelopab4  44792  eqsbc2VD  45080  fzisoeu  45548  iuneqfzuz  45580  supxrleubrnmptf  45695  rexanuz2nf  45736  fsummulc1f  45817  fsumiunss  45821  fmul01lt1lem2  45831  sumnnodd  45876  fnlimfvre2  45921  limsupreuz  45981  limsupvaluz2  45982  liminfvalxr  46027  icccncfext  46131  cncfiooicc  46138  cncfioobdlem  46140  dvmptmulf  46181  dvmptfprodlem  46188  volioc  46216  itgioocnicc  46221  fourierdlem12  46363  fourierdlem20  46371  fourierdlem25  46376  fourierdlem33  46384  fourierdlem42  46393  fourierdlem52  46402  fourierdlem54  46404  fourierdlem57  46407  fourierdlem58  46408  fourierdlem59  46409  fourierdlem63  46413  fourierdlem65  46415  fourierdlem68  46418  fourierdlem73  46423  fourierdlem74  46424  fourierdlem75  46425  fourierdlem80  46430  fourierdlem81  46431  rrndistlt  46534  sge0ltfirpmpt2  46670  sge0pnfmpt  46689  hoidmv1le  46838  hoidmvle  46844  vonioolem2  46925  smflimlem3  47017  chnsubseqwl  47123  lambert0  47133  lamberte  47134  euabsneu  47274  funressnfv  47289  aiotaval  47341  reuf1odnf  47353  reuf1od  47354  afvpcfv0  47392  dfafn5a  47406  afvelrnb  47409  afvelrnb0  47410  dfaimafn2  47412  dfatsnafv2  47498  dfatdmfcoafv2  47500  f1oresf1o2  47537  ceilbi  47579  minusmodnep2tmod  47599  0nelsetpreimafv  47636  fargshiftfo  47688  sprsymrelf1  47742  reupr  47768  fmtnorec2lem  47788  fmtnoprmfac1  47811  fmtnoprmfac2  47813  sfprmdvdsmersenne  47849  lighneallem2  47852  dfeven2  47895  dfodd3  47896  odd2np1ALTV  47920  even3prm2  47965  fppr2odd  47977  nnsum3primesgbe  48038  nnsum3primesle9  48040  clnbgrsym  48084  dfvopnbgr2  48099  isuspgrim0  48140  isuspgrimlem  48141  dfgric2  48161  grtriprop  48187  uspgrlimlem3  48236  gpgvtxedg1  48310  pgnbgreunbgrlem2lem1  48360  pgnbgreunbgrlem2lem2  48361  0nodd  48416  2nodd  48418  lmod0rng  48475  rngcinvALTV  48522  ringcinvALTV  48556  lcoel0  48674  lindslinindimp2lem4  48707  ldepspr  48719  lincresunit3  48727  nn0sumshdiglemB  48866  nn0sumshdiglem1  48867  rrx2pnedifcoorneorr  48963  eenglngeehlnmlem1  48983  eenglngeehlnmlem2  48984  rrx2linest  48988  rrx2linest2  48990  rrxsphere  48994  line2ylem  48997  line2x  49000  itscnhlc0xyqsol  49011  itschlc0xyqsol1  49012  itsclinecirc0b  49020  2itscp  49027  inlinecirc02plem  49032  brab2dd  49073  uptr2  49466