Theorem eqcom 2746

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

Syntax hints:   ↔ wb 207   = wceq 1547

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2731

This theorem is referenced by:  eqcoms  2747  eqcomi  2748  neqcomd  2749  eqeq2d  2750  eqabcbw  2813  eqabcb  2879  necom  2987  nesym  2990  gencbvex  3488  clel5  3603  eqsbc2  3786  dfss  3902  sspsstri  4036  ssdifim  4201  disj4  4387  reuprg0  4634  preq1b  4777  invdisj  5058  disjprg  5068  dtruALT  5317  reusv3  5334  opthg2  5419  copsex2g  5434  copsex4g  5436  opcom  5442  opeqsng  5444  opeqpr  5446  snopeqop  5447  propeqop  5448  opthwiener  5455  vopelopabsb  5471  opthprc  5682  elxp3  5684  relop  5792  dmopab3  5861  rnopab3  5898  rncoeq  5924  restidsing  6005  somin1  6083  xpcan  6127  xpcan2  6128  dfrel4v  6141  dmsnn0  6158  reu3op  6243  reuop  6244  opreu2reurex  6245  ordtri2  6345  ordtri2or3  6412  suc11  6419  on0eqel  6435  snsn0non  6436  iota1  6464  iotan0  6475  sniota  6476  mptfnf  6620  fresaunres1  6700  dffn5  6885  fvelrnb  6887  dfimafn2  6890  funimass4  6891  feqmptdf  6897  fnsnfv  6906  dmfco  6923  funcnvmpt  6937  fndmdif  6983  fneqeql  6987  rexrn  7028  ralrn  7029  elrnrexdmb  7031  dffo4  7044  fssrescdmd  7068  funopsn  7090  funopsnOLD  7091  ftpg  7099  fprb  7138  ralima  7181  reximaOLD  7183  ralimaOLD  7184  fvclss  7185  dff13  7198  f1eqcocnv  7245  fnssintima  7306  imaeqsexvOLD  7307  riotaeqimp  7339  eusvobj2  7348  f1ocnvfv3  7351  oprabidw  7387  oprabid  7388  oprabv  7416  eloprabga  7465  ovelimab  7534  onmindif2  7750  br1steqg  7953  br2ndeqg  7954  dfoprab3  7996  opiota  8001  f1o2ndf1  8061  soseq  8099  brtpos2  8172  tpossym  8198  mpocurryd  8209  rdglim2  8361  tz7.48lem  8370  oaf1o  8488  omopthi  8587  erth2  8689  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  9531  inf3lem2  9541  inf3lem6  9545  ttrcltr  9628  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  10689  psslinpr  10945  ltexprlem4  10953  ltsrpr  10991  mulgt0sr  11019  elreal  11045  ltresr  11054  leloe  11223  eqlei2  11248  addsubeq4  11399  subcan2  11410  negcon1  11437  negcon2  11438  addid0  11560  addeq0  11564  divmul2  11804  conjmul  11863  rereccl  11864  creur  12144  creui  12145  ind1a  12161  nndiv  12214  nn0sub  12478  elnn0z  12528  elznn0  12530  xrleloe  13086  ngtmnft  13109  icoshftf1o  13418  iccf1o  13440  fzen  13486  fzneuz  13553  injresinj  13737  fleqceilz  13804  mod0  13826  modmuladdnn0  13868  modirr  13895  addmodlteq  13899  nn0ennn  13932  hashrabsn01  14326  hashsdom  14334  hashgt12el2  14376  hashbclem  14405  hashfacen  14407  hashf1lem1  14408  hashtpg  14438  tpf1o  14454  fi1uzind  14460  ccatw2s1p1  14590  wrd2ind  14676  cshw1  14775  cshwsexa  14777  scshwfzeqfzo  14779  s2f1o  14869  wwlktovfo  14911  dmtrclfv  14971  cjreb  15076  leabs  15252  reusq0  15418  incexc2  15794  rpnnen2lem12  16183  dvdsval2  16215  dvdsabseq  16273  dvdsflip  16277  odd2np1  16301  oddm1even  16303  sqoddm1div8z  16314  m1exp1  16336  divalglem4  16356  divalglem8  16360  divalgb  16364  modremain  16368  zeqzmulgcd  16470  dfgcd2  16506  lcmfpr  16587  lcmftp  16596  lcmfunsnlem2  16600  divgcdcoprm0  16625  prm2orodd  16651  hashdvds  16736  oddprmdvds  16865  vdwlem12  16954  cshwshashlem1  17057  cshwsiun  17061  initoid  17959  termoid  17960  setcinv  18048  yonedainv  18238  joinfval  18328  joinfval2  18329  meetfval  18342  meetfval2  18343  latnle  18430  chnfi  18591  sgrp2nmndlem3  18887  grpid  18942  grpinvcnv  18973  grplmulf1o  18980  grpraddf1o  18981  grpsubeq0  18993  grpsubadd  18995  grplactcnv  19010  ressmulgnnd  19045  isnsg4  19133  eqg0el  19149  cycsubmel  19166  conjghm  19215  conjnmzb  19219  gacan  19271  gapm  19272  cntzrec  19302  oppgcntz  19330  fvcosymgeq  19395  odmulgeq  19523  dfod2  19530  sylow3lem3  19595  sylow3lem6  19598  lssnle  19640  lsmhash  19671  efgredlemb  19712  efgrelexlemb  19716  dprd2d2  20012  ablfac1eulem  20040  pgpfac1lem2  20043  pgpfac1lem4  20046  dvdsrval  20332  dvdsr02  20343  01eq0ring  20502  0ring01eqbi  20504  rngcinv  20609  ringcinv  20643  orngsqr  20838  rmodislmodlem  20919  lvecinv  21106  rngqiprngimf1lem  21287  rspsn  21326  prmirredlem  21447  zndvds  21524  znleval  21529  psrbagconf1o  21904  mplmonmul  22012  gsummoncoe1  22294  evl1maprhm  22365  mat1dimelbas  22454  mat1dimbas  22455  1mavmul  22531  ma1repveval  22554  mulmarep1gsum1  22556  mdetunilem9  22603  m2cpminvid2lem  22737  pmatcollpw3lem  22766  mp2pm2mplem4  22792  toponsspwpw  22905  dmtopon  22906  cmpfi  23391  ssref  23495  qtopeu  23699  hmeoimaf1o  23753  txhmeo  23786  fbasrn  23867  rnelfmlem  23935  hauspwpwf1  23970  alexsubALTlem4  24033  qustgpopn  24103  qustgphaus  24106  fmucndlem  24273  isngp3  24581  isngp4  24595  metnrmlem1a  24842  icopnfcnv  24927  iccpnfcnv  24929  ivthle  25441  ivthle2  25442  dyadmbl  25585  mbfinf  25650  i1fmulclem  25687  itg1mulc  25689  mvth  25977  dvivth  25995  lhop2  26000  r1pid2  26145  dvdsq1p  26146  reeff1o  26430  coseq1  26507  recosf1o  26517  resinf1o  26518  efopn  26640  cxpeq  26739  logreclem  26744  affineequiv  26805  affineequiv4  26808  affineequivne  26809  quad2  26821  dcubic  26828  mcubic  26829  quart  26843  atandm2  26859  rlimcnp2  26948  amgm  26972  wilthlem2  27050  mumullem2  27161  sqff1o  27163  dvdsflf1o  27168  gausslemma2dlem0i  27345  lgseisenlem2  27357  lgsquadlem2  27362  2lgslem1c  27374  2lgsoddprmlem2  27390  2lgsoddprm  27397  2sq2  27414  addsq2reu  27421  2sqreultlem  27428  2sqreunnltlem  27431  2sqreulem3  27434  ltsval2  27638  ltsintdifex  27643  ltsres  27644  nosepon  27647  noextenddif  27650  nosepssdm  27668  nogt01o  27678  nosupprefixmo  27682  noinfprefixmo  27683  nosupno  27685  noinfno  27700  lesloe  27736  eqcuts2  27796  cutbdaylt  27808  elold  27869  made0  27873  lrrecfr  27953  subadds  28080  oncutlt  28274  z12sge0  28493  renegscl  28508  tgjustf  28559  legtrid  28677  legso  28685  islmib  28873  lmicom  28874  lmiinv  28878  lmimid  28880  lmiopp  28888  colinearalglem2  28994  colinearalg  28997  ax5seglem4  29019  ax5seglem5  29020  axlowdimlem13  29041  axeuclidlem  29049  axeuclid  29050  axcontlem2  29052  axcontlem4  29054  elntg2  29072  structiedg0val  29109  uspgredgiedg  29262  uspgriedgedg  29263  usgredgsscusgredg  29546  fusgrn0degnn0  29586  umgr2v2evtxel  29609  vdiscusgrb  29617  uspgr2wlkeq  29732  wlk0prc  29739  wlklenvclwlk  29740  wlkp1lem8  29765  spthdep  29820  usgr2pthlem  29849  usgr2pth  29850  wlkiswwlksupgr2  29963  wlklnwwlkln2lem  29968  wwlksnextproplem3  29997  umgr2adedgwlk  30031  umgr2adedgspth  30034  umgr2wlkon  30036  usgrwwlks2on  30044  umgrwwlks2on  30045  elwwlks2  30055  elwspths2spth  30056  clwlkclwwlklem2a4  30085  clwlkclwwlklem2  30088  erclwwlkref  30108  clwwlkf  30135  erclwwlknref  30157  erclwwlknsym  30158  erclwwlkntr  30159  hashecclwwlkn1  30165  umgrhashecclwwlk  30166  eupth2lem2  30307  eucrct2eupth  30333  numclwwlkqhash  30463  isgrpo  30586  hvsubaddi  31155  hire  31183  shmodsi  31478  omlsilem  31491  chcon1i  31554  chnlei  31574  pjoml3i  31675  cmbr2i  31685  chscllem2  31727  adjsym  31922  eigorthi  31926  dfadj2  31974  adjval2  31980  cnvadj  31981  dmadjrnb  31995  adjvalval  32026  cnlnadjeui  32166  cnlnssadj  32169  adjbdln  32172  pjimai  32265  pjin2i  32282  pjin3i  32283  stadd3i  32337  largei  32356  cvnbtwn3  32377  cvnbtwn4  32378  mddmd2  32398  superpos  32443  atnemeq0  32466  sumdmdii  32504  sumdmdlem  32507  addltmulALT  32535  opreu2reuALT  32564  foresf1o  32592  difeq  32606  disjrdx  32680  fcoinvbr  32694  brab2d  32697  fmptco1f1o  32725  dfimafnf  32728  curry2ima  32801  intimafv  32803  receqid  32836  elicoelioo  32870  fzo0opth  32895  wrdt2ind  33032  swrdrn3  33034  gsummptp1  33138  gsummulsubdishift1  33149  cntrval2  33252  domnprodeq0  33357  qusker  33432  dvdsrspss  33470  lsmsnorb  33474  1arithufdlem4  33630  r1pid2OLD  33692  selvply1rhmlemb  33703  psrmonmul  33734  esplyind  33759  algextdeglem8  33908  zarcls  34058  xrmulc1cn  34114  xrge0iifcnv  34117  esumfsup  34254  esumpcvgval  34262  esumcvg  34270  esum2dlem  34276  issgon  34307  eulerpartgbij  34556  eulerpartlemgh  34562  ballotlemsima  34700  bnj1366  35011  bnj553  35080  bnj964  35125  fineqvnttrclse  35305  cusgredgex  35350  revwlk  35353  loop1cycl  35365  subfacp1lem3  35410  subfacp1lem5  35412  erdszelem9  35427  prv1n  35659  ply1divalg3  35870  quad3  35898  br6  35985  elintfv  35993  dfon2lem5  36013  dfon2lem8  36016  brbigcup  36124  dfbigcup2  36125  elfix  36129  ellimits  36136  snelsingles  36148  dfiota3  36149  imageval  36156  brapply  36164  lemsuccf  36167  dfsuccf2  36169  funpartlem  36170  brfullfun  36176  dfrecs2  36178  dfrdg4  36179  altopthbg  36196  altopthc  36199  altopthd  36200  altopelaltxp  36204  brsegle  36336  outsideofrflx  36355  elicc3  36545  nn0prpw  36551  opnregcld  36558  cldregopn  36559  fneval  36580  topfneec  36583  knoppndvlem9  36826  bj-elgab  37292  bj-gabima  37293  bj-elsngl  37321  bj-snglc  37322  bj-projval  37349  bj-disj2r  37381  bj-restreg  37457  bj-0int  37459  copsex2gd  37498  copsex2b  37500  bj-inftyexpitaudisj  37565  bj-inftyexpidisj  37570  bj-bary1lem1  37671  topdifinffinlem  37709  topdifinfeq  37712  fvineqsnf1  37772  curf  37965  uncf  37966  curunc  37969  unccur  37970  poimirlem2  37989  poimirlem16  38003  poimirlem17  38004  poimirlem19  38006  poimirlem20  38007  poimirlem27  38014  mblfinlem2  38025  mbfresfi  38033  itg2addnclem2  38039  ftc1anclem3  38062  fdc  38112  heibor1  38177  opidonOLD  38219  0rngo  38394  smprngopr  38419  isfldidl  38435  isfldidl2  38436  eqbrb  38606  eqelb  38608  ideq2  38680  relcnveq  38695  n0elqs  38699  disjressuc2  38778  dfsucmap3  38830  dfsucmap4  38832  dmsucmap  38835  preuniqval  38863  elrelscnveq  38995  qseq  39100  disjdmqscossss  39273  lcvnbtwn3  39520  lcvexchlem1  39526  lsatnem0  39537  opcon1b  39690  omllaw2N  39736  cmtbr2N  39745  leatb  39784  cvlsupr2  39835  glbconxN  39870  islln3  40002  llnexatN  40013  islpln3  40025  lplnexatN  40055  islvol3  40068  dalem-cly  40163  isline4N  40269  2llnma3r  40280  poml4N  40445  4atex2  40569  4atex2-0bOLDN  40571  cdlemefrs29bpre0  40888  cdlemftr3  41057  cdlemb3  41098  cdlemg17h  41160  cdlemg17pq  41164  cdlemg19  41176  cdlemg21  41178  tendoex  41467  dva1dim  41477  dihglb2  41834  doch11  41865  dochsordN  41866  lcfrlem9  42042  hlhillcs  42450  lcmineqlem4  42517  aks6d1c7lem2  42666  aks5lem3a  42674  aks5lem6  42677  unitscyglem2  42681  unitscyglem3  42682  addsubeq4com  42757  ef11d  42816  redivmul2d  42923  fimgmcyclem  43019  fsuppind  43040  elrfirn  43144  isnacs2  43155  isnacs3  43159  fiphp3d  43264  wopprc  43475  islnm2  43523  kercvrlsm  43528  fgraphopab  43648  tfsconcatlem  43781  tfsconcatrn  43787  tfsconcat0i  43790  tfsconcat0b  43791  tfsconcatrev  43793  oaun3lem1  43819  oadif1lem  43824  oadif1  43825  rp-fakeuninass  43960  snen1g  43968  iscard4  43977  sqrtcval  44085  frege124d  44205  frege129d  44207  frege92  44399  dffrege99  44406  clsk3nimkb  44484  clsk1indlem4  44488  clsk1indlem1  44489  ntrclsiso  44511  ntrclsk3  44514  ntrclsk13  44515  ntrneik4w  44544  extoimad  44608  int-sqdefd  44625  int-sqgeq0d  44630  radcnvrat  44758  bcc0  44784  opelopab4  44995  eqsbc2VD  45283  fzisoeu  45748  iuneqfzuz  45780  supxrleubrnmptf  45894  rexanuz2nf  45935  fsummulc1f  46016  fsumiunss  46020  fmul01lt1lem2  46030  sumnnodd  46075  fnlimfvre2  46120  limsupreuz  46180  limsupvaluz2  46181  liminfvalxr  46226  icccncfext  46330  cncfiooicc  46337  cncfioobdlem  46339  dvmptmulf  46380  dvmptfprodlem  46387  volioc  46415  itgioocnicc  46420  fourierdlem12  46562  fourierdlem20  46570  fourierdlem25  46575  fourierdlem33  46583  fourierdlem42  46592  fourierdlem52  46601  fourierdlem54  46603  fourierdlem57  46606  fourierdlem58  46607  fourierdlem59  46608  fourierdlem63  46612  fourierdlem65  46614  fourierdlem68  46617  fourierdlem73  46622  fourierdlem74  46623  fourierdlem75  46624  fourierdlem80  46629  fourierdlem81  46630  rrndistlt  46733  sge0ltfirpmpt2  46869  sge0pnfmpt  46888  hoidmv1le  47037  hoidmvle  47043  vonioolem2  47124  smflimlem3  47216  chnsubseqwl  47324  cos5teq  47343  lambert0  47350  lamberte  47351  euabsneu  47491  funressnfv  47506  aiotaval  47558  reuf1odnf  47570  reuf1od  47571  afvpcfv0  47609  dfafn5a  47623  afvelrnb  47626  afvelrnb0  47627  dfaimafn2  47629  dfatsnafv2  47715  dfatdmfcoafv2  47717  f1oresf1o2  47754  ceilbi  47800  minusmodnep2tmod  47822  0nelsetpreimafv  47865  fargshiftfo  47917  sprsymrelf1  47971  reupr  47997  nprmmul1  48002  fmtnorec2lem  48020  fmtnoprmfac1  48043  fmtnoprmfac2  48045  sfprmdvdsmersenne  48081  lighneallem2  48084  dfeven2  48140  dfodd3  48141  odd2np1ALTV  48165  even3prm2  48210  fppr2odd  48222  nnsum3primesgbe  48283  nnsum3primesle9  48285  clnbgrsym  48329  dfvopnbgr2  48344  isuspgrim0  48385  isuspgrimlem  48386  dfgric2  48406  grtriprop  48432  uspgrlimlem3  48481  gpgvtxedg1  48555  pgnbgreunbgrlem2lem1  48605  pgnbgreunbgrlem2lem2  48606  0nodd  48661  2nodd  48663  lmod0rng  48720  rngcinvALTV  48767  ringcinvALTV  48801  lcoel0  48919  lindslinindimp2lem4  48952  ldepspr  48964  lincresunit3  48972  nn0sumshdiglemB  49111  nn0sumshdiglem1  49112  rrx2pnedifcoorneorr  49208  eenglngeehlnmlem1  49228  eenglngeehlnmlem2  49229  rrx2linest  49233  rrx2linest2  49235  rrxsphere  49239  line2ylem  49242  line2x  49245  itscnhlc0xyqsol  49256  itschlc0xyqsol1  49257  itsclinecirc0b  49265  2itscp  49272  inlinecirc02plem  49277  brab2dd  49318  uptr2  49711