Theorem eqcom 2744

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

Syntax hints:   ↔ wb 206   = wceq 1540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2729

This theorem is referenced by:  eqcoms  2745  eqcomi  2746  neqcomd  2747  eqeq2d  2748  eqtr2OLD  2762  eqtr3OLD  2764  eqabcb  2883  necom  2994  nesym  2997  pm13.181OLD  3024  gencbvex  3541  clel5  3665  eqsbc2  3854  dfss  3970  sspsstri  4105  ssnelpss  4114  ssdifim  4273  disj  4450  disj4  4459  reuprg0  4702  preq1b  4846  invdisj  5129  disjprg  5139  dtruALT  5388  reusv3  5405  opthg2  5484  copsex2g  5498  copsex4g  5500  opcom  5506  opeqsng  5508  opeqpr  5510  snopeqop  5511  propeqop  5512  opthwiener  5519  vopelopabsb  5534  opthprc  5749  elxp3  5751  relop  5861  dmopab3  5930  rnopab3  5967  rncoeq  5990  restidsing  6071  somin1  6153  xpcan  6196  xpcan2  6197  dfrel4v  6210  dmsnn0  6227  reu3op  6312  reuop  6313  opreu2reurex  6314  ordtri2  6419  ordtri2or3  6484  suc11  6491  on0eqel  6508  snsn0non  6509  iota1  6538  iotan0  6551  sniota  6552  mptfnf  6703  fresaunres1  6781  dffn5  6967  fvelrnb  6969  dfimafn2  6972  funimass4  6973  feqmptdf  6979  fnsnfv  6988  dmfco  7005  fndmdif  7062  fneqeql  7066  rexrn  7107  ralrn  7108  elrnrexdmb  7110  dffo4  7123  fssrescdmd  7146  funopsn  7168  ftpg  7176  fprb  7214  ralima  7257  reximaOLD  7259  ralimaOLD  7260  fvclss  7261  dff13  7275  f1eqcocnv  7321  fnssintima  7382  imaeqsexvOLD  7383  riotaeqimp  7414  eusvobj2  7423  f1ocnvfv3  7426  oprabidw  7462  oprabid  7463  oprabv  7493  eloprabga  7542  ovelimab  7611  onmindif2  7827  br1steqg  8036  br2ndeqg  8037  dfoprab3  8079  opiota  8084  f1o2ndf1  8147  soseq  8184  brtpos2  8257  tpossym  8283  mpocurryd  8294  rdglim2  8472  tz7.48lem  8481  oaf1o  8601  omopthi  8699  erth2  8797  brecop  8850  erovlem  8853  ecopovsym  8859  eceqoveq  8862  xpcomco  9102  omxpenlem  9113  mapen  9181  nneneq  9246  nneneqOLD  9258  unxpdomlem3  9288  unfilem1  9343  mapfien  9448  supgtoreq  9510  wemapsolem  9590  suc11reg  9659  inf3lem2  9669  inf3lem6  9673  ttrcltr  9756  djulf1o  9952  djurf1o  9953  infenaleph  10131  isinfcard  10132  dfac5  10169  cfeq0  10296  cfsuc  10297  ssfin4  10350  fin23lem25  10364  fin23lem22  10367  fin23lem40  10391  fin1a2lem5  10444  axcclem  10497  brdom7disj  10571  brdom6disj  10572  inar1  10815  psslinpr  11071  ltexprlem4  11079  ltsrpr  11117  mulgt0sr  11145  elreal  11171  ltresr  11180  leloe  11347  eqlei2  11372  addsubeq4  11523  subcan2  11534  negcon1  11561  negcon2  11562  addid0  11682  addeq0  11686  divmul2  11926  conjmul  11984  rereccl  11985  creur  12260  creui  12261  nndiv  12312  nn0sub  12576  elnn0z  12626  elznn0  12628  xrleloe  13186  ngtmnft  13208  icoshftf1o  13514  iccf1o  13536  fzen  13581  fzneuz  13648  injresinj  13827  fleqceilz  13894  mod0  13916  modmuladdnn0  13956  modirr  13983  addmodlteq  13987  nn0ennn  14020  hashrabsn01  14412  hashsdom  14420  hashgt12el2  14462  hashbclem  14491  hashfacen  14493  hashf1lem1  14494  hashtpg  14524  tpf1o  14540  fi1uzind  14546  ccatw2s1p1  14674  wrd2ind  14761  cshw1  14860  cshwsexa  14862  scshwfzeqfzo  14865  s2f1o  14955  wwlktovfo  14997  dmtrclfv  15057  cjreb  15162  leabs  15338  reusq0  15501  incexc2  15874  rpnnen2lem12  16261  dvdsval2  16293  dvdsabseq  16350  dvdsflip  16354  odd2np1  16378  oddm1even  16380  sqoddm1div8z  16391  m1exp1  16413  divalglem4  16433  divalglem8  16437  divalgb  16441  modremain  16445  zeqzmulgcd  16547  dfgcd2  16583  lcmfpr  16664  lcmftp  16673  lcmfunsnlem2  16677  divgcdcoprm0  16702  prm2orodd  16728  hashdvds  16812  oddprmdvds  16941  vdwlem12  17030  cshwshashlem1  17133  cshwsiun  17137  initoid  18046  termoid  18047  setcinv  18135  yonedainv  18326  joinfval  18418  joinfval2  18419  meetfval  18432  meetfval2  18433  latnle  18518  sgrp2nmndlem3  18938  grpid  18993  grpinvcnv  19024  grplmulf1o  19031  grpraddf1o  19032  grpsubeq0  19044  grpsubadd  19046  grplactcnv  19061  ressmulgnnd  19096  isnsg4  19185  eqg0el  19201  cycsubmel  19218  conjghm  19267  conjnmzb  19271  gacan  19323  gapm  19324  cntzrec  19354  oppgcntz  19383  fvcosymgeq  19447  odmulgeq  19575  dfod2  19582  sylow3lem3  19647  sylow3lem6  19650  lssnle  19692  lsmhash  19723  efgredlemb  19764  efgrelexlemb  19768  dprd2d2  20064  ablfac1eulem  20092  pgpfac1lem2  20095  pgpfac1lem4  20098  dvdsrval  20361  dvdsr02  20372  01eq0ring  20530  0ring01eqbi  20532  rngcinv  20637  ringcinv  20671  rmodislmodlem  20927  lvecinv  21115  rngqiprngimf1lem  21304  rspsn  21343  dfcnfldOLD  21380  prmirredlem  21483  zndvds  21568  znleval  21573  psrbagconf1o  21949  mplmonmul  22054  gsummoncoe1  22312  evl1maprhm  22383  mat1dimelbas  22477  mat1dimbas  22478  1mavmul  22554  ma1repveval  22577  mulmarep1gsum1  22579  mdetunilem9  22626  m2cpminvid2lem  22760  pmatcollpw3lem  22789  mp2pm2mplem4  22815  toponsspwpw  22928  dmtopon  22929  cmpfi  23416  ssref  23520  qtopeu  23724  hmeoimaf1o  23778  txhmeo  23811  fbasrn  23892  rnelfmlem  23960  hauspwpwf1  23995  alexsubALTlem4  24058  qustgpopn  24128  qustgphaus  24131  fmucndlem  24300  isngp3  24611  isngp4  24625  metnrmlem1a  24880  icopnfcnv  24973  iccpnfcnv  24975  ivthle  25491  ivthle2  25492  dyadmbl  25635  mbfinf  25700  i1fmulclem  25737  itg1mulc  25739  mvth  26031  dvivth  26049  lhop2  26054  r1pid2  26201  dvdsq1p  26202  reeff1o  26491  coseq1  26567  recosf1o  26577  resinf1o  26578  efopn  26700  cxpeq  26800  logreclem  26805  affineequiv  26866  affineequiv4  26869  affineequivne  26870  quad2  26882  dcubic  26889  mcubic  26890  quart  26904  atandm2  26920  rlimcnp2  27009  amgm  27034  wilthlem2  27112  mumullem2  27223  sqff1o  27225  dvdsflf1o  27230  gausslemma2dlem0i  27408  lgseisenlem2  27420  lgsquadlem2  27425  2lgslem1c  27437  2lgsoddprmlem2  27453  2lgsoddprm  27460  2sq2  27477  addsq2reu  27484  2sqreultlem  27491  2sqreunnltlem  27494  2sqreulem3  27497  sltval2  27701  sltintdifex  27706  sltres  27707  nosepon  27710  noextenddif  27713  nosepssdm  27731  nogt01o  27741  nosupprefixmo  27745  noinfprefixmo  27746  nosupno  27748  noinfno  27763  sleloe  27799  eqscut2  27851  scutbdaylt  27863  elold  27908  made0  27912  lrrecfr  27976  subadds  28100  cutpw2  28417  renegscl  28430  tgjustf  28481  legtrid  28599  legso  28607  islmib  28795  lmicom  28796  lmiinv  28800  lmimid  28802  lmiopp  28810  colinearalglem2  28922  colinearalg  28925  ax5seglem4  28947  ax5seglem5  28948  axlowdimlem13  28969  axeuclidlem  28977  axeuclid  28978  axcontlem2  28980  axcontlem4  28982  elntg2  29000  structiedg0val  29039  uspgredgiedg  29192  uspgriedgedg  29193  usgredgsscusgredg  29477  fusgrn0degnn0  29517  umgr2v2evtxel  29540  vdiscusgrb  29548  uspgr2wlkeq  29664  wlk0prc  29672  wlklenvclwlk  29673  wlkp1lem8  29698  spthdep  29754  usgr2pthlem  29783  usgr2pth  29784  wlkiswwlksupgr2  29897  wlklnwwlkln2lem  29902  wwlksnextproplem3  29931  umgr2adedgwlk  29965  umgr2adedgspth  29968  umgr2wlkon  29970  umgrwwlks2on  29977  elwwlks2  29986  elwspths2spth  29987  clwlkclwwlklem2a4  30016  clwlkclwwlklem2  30019  erclwwlkref  30039  clwwlkf  30066  erclwwlknref  30088  erclwwlknsym  30089  erclwwlkntr  30090  hashecclwwlkn1  30096  umgrhashecclwwlk  30097  eupth2lem2  30238  eucrct2eupth  30264  numclwwlkqhash  30394  isgrpo  30516  hvsubaddi  31085  hire  31113  shmodsi  31408  omlsilem  31421  chcon1i  31484  chnlei  31504  pjoml3i  31605  cmbr2i  31615  chscllem2  31657  adjsym  31852  eigorthi  31856  dfadj2  31904  adjval2  31910  cnvadj  31911  dmadjrnb  31925  adjvalval  31956  cnlnadjeui  32096  cnlnssadj  32099  adjbdln  32102  pjimai  32195  pjin2i  32212  pjin3i  32213  stadd3i  32267  largei  32286  cvnbtwn3  32307  cvnbtwn4  32308  mddmd2  32328  superpos  32373  atnemeq0  32396  sumdmdii  32434  sumdmdlem  32437  addltmulALT  32465  opreu2reuALT  32496  foresf1o  32523  difeq  32537  disjrdx  32604  fcoinvbr  32618  brab2d  32619  fmptco1f1o  32643  dfimafnf  32646  funcnvmpt  32677  curry2ima  32718  intimafv  32720  elicoelioo  32780  fzo0opth  32807  ind1a  32844  wrdt2ind  32938  swrdrn3  32940  orngsqr  33334  qusker  33377  dvdsrspss  33415  lsmsnorb  33419  1arithufdlem4  33575  r1pid2OLD  33629  algextdeglem8  33765  zarcls  33873  xrmulc1cn  33929  xrge0iifcnv  33932  esumfsup  34071  esumpcvgval  34079  esumcvg  34087  esum2dlem  34093  issgon  34124  eulerpartgbij  34374  eulerpartlemgh  34380  ballotlemsima  34518  bnj1366  34843  bnj553  34912  bnj964  34957  cusgredgex  35127  revwlk  35130  loop1cycl  35142  subfacp1lem3  35187  subfacp1lem5  35189  erdszelem9  35204  prv1n  35436  ply1divalg3  35647  quad3  35675  br6  35757  elintfv  35765  dfon2lem5  35788  dfon2lem8  35791  brbigcup  35899  dfbigcup2  35900  elfix  35904  ellimits  35911  snelsingles  35923  dfiota3  35924  imageval  35931  brapply  35939  brsuccf  35942  funpartlem  35943  brfullfun  35949  dfrecs2  35951  dfrdg4  35952  altopthbg  35969  altopthc  35972  altopthd  35973  altopelaltxp  35977  brsegle  36109  outsideofrflx  36128  elicc3  36318  nn0prpw  36324  opnregcld  36331  cldregopn  36332  fneval  36353  topfneec  36356  knoppndvlem9  36521  bj-elgab  36940  bj-gabima  36941  bj-elsngl  36969  bj-snglc  36970  bj-projval  36997  bj-disj2r  37029  bj-restreg  37100  bj-0int  37102  copsex2b  37141  bj-inftyexpitaudisj  37206  bj-inftyexpidisj  37211  bj-bary1lem1  37312  topdifinffinlem  37348  topdifinfeq  37351  fvineqsnf1  37411  curf  37605  uncf  37606  curunc  37609  unccur  37610  poimirlem2  37629  poimirlem16  37643  poimirlem17  37644  poimirlem19  37646  poimirlem20  37647  poimirlem27  37654  mblfinlem2  37665  mbfresfi  37673  itg2addnclem2  37679  ftc1anclem3  37702  fdc  37752  heibor1  37817  opidonOLD  37859  0rngo  38034  smprngopr  38059  isfldidl  38075  isfldidl2  38076  eqbrb  38234  eqelb  38236  ideq2  38308  relcnveq  38323  n0elqs  38327  disjressuc2  38389  elrelscnveq  38493  disjdmqscossss  38804  lcvnbtwn3  39029  lcvexchlem1  39035  lsatnem0  39046  opcon1b  39199  omllaw2N  39245  cmtbr2N  39254  leatb  39293  cvlsupr2  39344  glbconxN  39380  islln3  39512  llnexatN  39523  islpln3  39535  lplnexatN  39565  islvol3  39578  dalem-cly  39673  isline4N  39779  2llnma3r  39790  poml4N  39955  4atex2  40079  4atex2-0bOLDN  40081  cdlemefrs29bpre0  40398  cdlemftr3  40567  cdlemb3  40608  cdlemg17h  40670  cdlemg17pq  40674  cdlemg19  40686  cdlemg21  40688  tendoex  40977  dva1dim  40987  dihglb2  41344  doch11  41375  dochsordN  41376  lcfrlem9  41552  hlhillcs  41964  lcmineqlem4  42033  aks6d1c7lem2  42182  aks5lem3a  42190  aks5lem6  42193  unitscyglem2  42197  unitscyglem3  42198  metakunt1  42206  metakunt6  42211  metakunt15  42220  metakunt16  42221  addsubeq4com  42315  ef11d  42375  fimgmcyclem  42543  fsuppind  42600  elrfirn  42706  isnacs2  42717  isnacs3  42721  fiphp3d  42830  wopprc  43042  islnm2  43090  kercvrlsm  43095  fgraphopab  43215  tfsconcatlem  43349  tfsconcatrn  43355  tfsconcat0i  43358  tfsconcat0b  43359  tfsconcatrev  43361  oaun3lem1  43387  oadif1lem  43392  oadif1  43393  rp-fakeuninass  43529  snen1g  43537  iscard4  43546  sqrtcval  43654  frege124d  43774  frege129d  43776  frege92  43968  dffrege99  43975  clsk3nimkb  44053  clsk1indlem4  44057  clsk1indlem1  44058  ntrclsiso  44080  ntrclsk3  44083  ntrclsk13  44084  ntrneik4w  44113  extoimad  44177  int-sqdefd  44194  int-sqgeq0d  44199  radcnvrat  44333  bcc0  44359  opelopab4  44571  eqsbc2VD  44860  fzisoeu  45312  iuneqfzuz  45346  supxrleubrnmptf  45462  rexanuz2nf  45503  fsummulc1f  45586  fsumiunss  45590  fmul01lt1lem2  45600  sumnnodd  45645  fnlimfvre2  45692  limsupreuz  45752  limsupvaluz2  45753  liminfvalxr  45798  icccncfext  45902  cncfiooicc  45909  cncfioobdlem  45911  dvmptmulf  45952  dvmptfprodlem  45959  volioc  45987  itgioocnicc  45992  fourierdlem12  46134  fourierdlem20  46142  fourierdlem25  46147  fourierdlem33  46155  fourierdlem42  46164  fourierdlem52  46173  fourierdlem54  46175  fourierdlem57  46178  fourierdlem58  46179  fourierdlem59  46180  fourierdlem63  46184  fourierdlem65  46186  fourierdlem68  46189  fourierdlem73  46194  fourierdlem74  46195  fourierdlem75  46196  fourierdlem80  46201  fourierdlem81  46202  rrndistlt  46305  sge0ltfirpmpt2  46441  sge0pnfmpt  46460  hoidmv1le  46609  hoidmvle  46615  vonioolem2  46696  smflimlem3  46788  euabsneu  47040  funressnfv  47055  aiotaval  47107  reuf1odnf  47119  reuf1od  47120  afvpcfv0  47158  dfafn5a  47172  afvelrnb  47175  afvelrnb0  47176  dfaimafn2  47178  dfatsnafv2  47264  dfatdmfcoafv2  47266  f1oresf1o2  47303  minusmodnep2tmod  47355  0nelsetpreimafv  47377  fargshiftfo  47429  sprsymrelf1  47483  reupr  47509  fmtnorec2lem  47529  fmtnoprmfac1  47552  fmtnoprmfac2  47554  sfprmdvdsmersenne  47590  lighneallem2  47593  dfeven2  47636  dfodd3  47637  odd2np1ALTV  47661  even3prm2  47706  fppr2odd  47718  nnsum3primesgbe  47779  nnsum3primesle9  47781  clnbgrsym  47824  dfvopnbgr2  47839  isuspgrim0  47872  isuspgrimlem  47874  dfgric2  47884  grtriprop  47908  uspgrlimlem3  47957  gpgvtxedg1  48022  0nodd  48086  2nodd  48088  lmod0rng  48145  rngcinvALTV  48192  ringcinvALTV  48226  lcoel0  48345  lindslinindimp2lem4  48378  ldepspr  48390  lincresunit3  48398  nn0sumshdiglemB  48541  nn0sumshdiglem1  48542  rrx2pnedifcoorneorr  48638  eenglngeehlnmlem1  48658  eenglngeehlnmlem2  48659  rrx2linest  48663  rrx2linest2  48665  rrxsphere  48669  line2ylem  48672  line2x  48675  itscnhlc0xyqsol  48686  itschlc0xyqsol1  48687  itsclinecirc0b  48695  2itscp  48702  inlinecirc02plem  48707  brab2dd  48741