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 1542

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

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

This theorem is referenced by:  eqcoms  2745  eqcomi  2746  neqcomd  2747  eqeq2d  2748  eqabcbw  2811  eqabcb  2877  necom  2986  nesym  2989  gencbvex  3501  clel5  3621  eqsbc2  3806  dfss  3922  sspsstri  4059  ssnelpss  4068  ssdifim  4227  disj4  4413  reuprg0  4661  preq1b  4804  invdisj  5086  disjprg  5096  dtruALT  5335  reusv3  5352  opthg2  5435  copsex2g  5449  copsex4g  5451  opcom  5457  opeqsng  5459  opeqpr  5461  snopeqop  5462  propeqop  5463  opthwiener  5470  vopelopabsb  5485  opthprc  5696  elxp3  5698  relop  5807  dmopab3  5876  rnopab3  5913  rncoeq  5939  restidsing  6020  somin1  6098  xpcan  6142  xpcan2  6143  dfrel4v  6156  dmsnn0  6173  reu3op  6258  reuop  6259  opreu2reurex  6260  ordtri2  6360  ordtri2or3  6427  suc11  6434  on0eqel  6450  snsn0non  6451  iota1  6479  iotan0  6490  sniota  6491  mptfnf  6635  fresaunres1  6715  dffn5  6900  fvelrnb  6902  dfimafn2  6905  funimass4  6906  feqmptdf  6912  fnsnfv  6921  dmfco  6938  funcnvmpt  6951  fndmdif  6996  fneqeql  7000  rexrn  7041  ralrn  7042  elrnrexdmb  7044  dffo4  7057  fssrescdmd  7081  funopsn  7103  ftpg  7111  fprb  7150  ralima  7193  reximaOLD  7195  ralimaOLD  7196  fvclss  7197  dff13  7210  f1eqcocnv  7257  fnssintima  7318  imaeqsexvOLD  7319  riotaeqimp  7351  eusvobj2  7360  f1ocnvfv3  7363  oprabidw  7399  oprabid  7400  oprabv  7428  eloprabga  7477  ovelimab  7546  onmindif2  7762  br1steqg  7965  br2ndeqg  7966  dfoprab3  8008  opiota  8013  f1o2ndf1  8074  soseq  8111  brtpos2  8184  tpossym  8210  mpocurryd  8221  rdglim2  8373  tz7.48lem  8382  oaf1o  8500  omopthi  8599  erth2  8701  brecop  8759  erovlem  8762  ecopovsym  8768  eceqoveq  8771  xpcomco  9007  omxpenlem  9018  mapen  9081  nneneq  9142  unxpdomlem3  9170  unfilem1  9217  mapfien  9323  supgtoreq  9386  wemapsolem  9467  suc11reg  9540  inf3lem2  9550  inf3lem6  9554  ttrcltr  9637  djulf1o  9836  djurf1o  9837  infenaleph  10013  isinfcard  10014  dfac5  10051  cfeq0  10178  cfsuc  10179  ssfin4  10232  fin23lem25  10246  fin23lem22  10249  fin23lem40  10273  fin1a2lem5  10326  axcclem  10379  brdom7disj  10453  brdom6disj  10454  inar1  10698  psslinpr  10954  ltexprlem4  10962  ltsrpr  11000  mulgt0sr  11028  elreal  11054  ltresr  11063  leloe  11231  eqlei2  11256  addsubeq4  11407  subcan2  11418  negcon1  11445  negcon2  11446  addid0  11568  addeq0  11572  divmul2  11812  conjmul  11870  rereccl  11871  creur  12151  creui  12152  nndiv  12203  nn0sub  12463  elnn0z  12513  elznn0  12515  xrleloe  13070  ngtmnft  13093  icoshftf1o  13402  iccf1o  13424  fzen  13469  fzneuz  13536  injresinj  13719  fleqceilz  13786  mod0  13808  modmuladdnn0  13850  modirr  13877  addmodlteq  13881  nn0ennn  13914  hashrabsn01  14308  hashsdom  14316  hashgt12el2  14358  hashbclem  14387  hashfacen  14389  hashf1lem1  14390  hashtpg  14420  tpf1o  14436  fi1uzind  14442  ccatw2s1p1  14572  wrd2ind  14658  cshw1  14757  cshwsexa  14759  scshwfzeqfzo  14761  s2f1o  14851  wwlktovfo  14893  dmtrclfv  14953  cjreb  15058  leabs  15234  reusq0  15400  incexc2  15773  rpnnen2lem12  16162  dvdsval2  16194  dvdsabseq  16252  dvdsflip  16256  odd2np1  16280  oddm1even  16282  sqoddm1div8z  16293  m1exp1  16315  divalglem4  16335  divalglem8  16339  divalgb  16343  modremain  16347  zeqzmulgcd  16449  dfgcd2  16485  lcmfpr  16566  lcmftp  16575  lcmfunsnlem2  16579  divgcdcoprm0  16604  prm2orodd  16630  hashdvds  16714  oddprmdvds  16843  vdwlem12  16932  cshwshashlem1  17035  cshwsiun  17039  initoid  17937  termoid  17938  setcinv  18026  yonedainv  18216  joinfval  18306  joinfval2  18307  meetfval  18320  meetfval2  18321  latnle  18408  chnfi  18569  sgrp2nmndlem3  18862  grpid  18917  grpinvcnv  18948  grplmulf1o  18955  grpraddf1o  18956  grpsubeq0  18968  grpsubadd  18970  grplactcnv  18985  ressmulgnnd  19020  isnsg4  19108  eqg0el  19124  cycsubmel  19141  conjghm  19190  conjnmzb  19194  gacan  19246  gapm  19247  cntzrec  19277  oppgcntz  19305  fvcosymgeq  19370  odmulgeq  19498  dfod2  19505  sylow3lem3  19570  sylow3lem6  19573  lssnle  19615  lsmhash  19646  efgredlemb  19687  efgrelexlemb  19691  dprd2d2  19987  ablfac1eulem  20015  pgpfac1lem2  20018  pgpfac1lem4  20021  dvdsrval  20309  dvdsr02  20320  01eq0ring  20475  0ring01eqbi  20477  rngcinv  20582  ringcinv  20616  orngsqr  20811  rmodislmodlem  20892  lvecinv  21080  rngqiprngimf1lem  21261  rspsn  21300  dfcnfldOLD  21337  prmirredlem  21439  zndvds  21516  znleval  21521  psrbagconf1o  21897  mplmonmul  22003  gsummoncoe1  22264  evl1maprhm  22335  mat1dimelbas  22427  mat1dimbas  22428  1mavmul  22504  ma1repveval  22527  mulmarep1gsum1  22529  mdetunilem9  22576  m2cpminvid2lem  22710  pmatcollpw3lem  22739  mp2pm2mplem4  22765  toponsspwpw  22878  dmtopon  22879  cmpfi  23364  ssref  23468  qtopeu  23672  hmeoimaf1o  23726  txhmeo  23759  fbasrn  23840  rnelfmlem  23908  hauspwpwf1  23943  alexsubALTlem4  24006  qustgpopn  24076  qustgphaus  24079  fmucndlem  24246  isngp3  24554  isngp4  24568  metnrmlem1a  24815  icopnfcnv  24908  iccpnfcnv  24910  ivthle  25425  ivthle2  25426  dyadmbl  25569  mbfinf  25634  i1fmulclem  25671  itg1mulc  25673  mvth  25965  dvivth  25983  lhop2  25988  r1pid2  26135  dvdsq1p  26136  reeff1o  26425  coseq1  26502  recosf1o  26512  resinf1o  26513  efopn  26635  cxpeq  26735  logreclem  26740  affineequiv  26801  affineequiv4  26804  affineequivne  26805  quad2  26817  dcubic  26824  mcubic  26825  quart  26839  atandm2  26855  rlimcnp2  26944  amgm  26969  wilthlem2  27047  mumullem2  27158  sqff1o  27160  dvdsflf1o  27165  gausslemma2dlem0i  27343  lgseisenlem2  27355  lgsquadlem2  27360  2lgslem1c  27372  2lgsoddprmlem2  27388  2lgsoddprm  27395  2sq2  27412  addsq2reu  27419  2sqreultlem  27426  2sqreunnltlem  27429  2sqreulem3  27432  ltsval2  27636  ltsintdifex  27641  ltsres  27642  nosepon  27645  noextenddif  27648  nosepssdm  27666  nogt01o  27676  nosupprefixmo  27680  noinfprefixmo  27681  nosupno  27683  noinfno  27698  lesloe  27734  eqcuts2  27794  cutbdaylt  27806  elold  27867  made0  27871  lrrecfr  27951  subadds  28078  oncutlt  28272  z12sge0  28491  renegscl  28506  tgjustf  28557  legtrid  28675  legso  28683  islmib  28871  lmicom  28872  lmiinv  28876  lmimid  28878  lmiopp  28886  colinearalglem2  28992  colinearalg  28995  ax5seglem4  29017  ax5seglem5  29018  axlowdimlem13  29039  axeuclidlem  29047  axeuclid  29048  axcontlem2  29050  axcontlem4  29052  elntg2  29070  structiedg0val  29107  uspgredgiedg  29260  uspgriedgedg  29261  usgredgsscusgredg  29545  fusgrn0degnn0  29585  umgr2v2evtxel  29608  vdiscusgrb  29616  uspgr2wlkeq  29731  wlk0prc  29738  wlklenvclwlk  29739  wlkp1lem8  29764  spthdep  29819  usgr2pthlem  29848  usgr2pth  29849  wlkiswwlksupgr2  29962  wlklnwwlkln2lem  29967  wwlksnextproplem3  29996  umgr2adedgwlk  30030  umgr2adedgspth  30033  umgr2wlkon  30035  usgrwwlks2on  30043  umgrwwlks2on  30044  elwwlks2  30054  elwspths2spth  30055  clwlkclwwlklem2a4  30084  clwlkclwwlklem2  30087  erclwwlkref  30107  clwwlkf  30134  erclwwlknref  30156  erclwwlknsym  30157  erclwwlkntr  30158  hashecclwwlkn1  30164  umgrhashecclwwlk  30165  eupth2lem2  30306  eucrct2eupth  30332  numclwwlkqhash  30462  isgrpo  30585  hvsubaddi  31154  hire  31182  shmodsi  31477  omlsilem  31490  chcon1i  31553  chnlei  31573  pjoml3i  31674  cmbr2i  31684  chscllem2  31726  adjsym  31921  eigorthi  31925  dfadj2  31973  adjval2  31979  cnvadj  31980  dmadjrnb  31994  adjvalval  32025  cnlnadjeui  32165  cnlnssadj  32168  adjbdln  32171  pjimai  32264  pjin2i  32281  pjin3i  32282  stadd3i  32336  largei  32355  cvnbtwn3  32376  cvnbtwn4  32377  mddmd2  32397  superpos  32442  atnemeq0  32465  sumdmdii  32503  sumdmdlem  32506  addltmulALT  32534  opreu2reuALT  32563  foresf1o  32591  difeq  32605  disjrdx  32678  fcoinvbr  32692  brab2d  32695  fmptco1f1o  32723  dfimafnf  32726  curry2ima  32799  intimafv  32801  receqid  32835  elicoelioo  32869  fzo0opth  32894  ind1a  32949  wrdt2ind  33046  swrdrn3  33048  gsummptp1  33151  gsummulsubdishift1  33162  cntrval2  33265  domnprodeq0  33370  qusker  33442  dvdsrspss  33480  lsmsnorb  33484  1arithufdlem4  33640  r1pid2OLD  33702  psrmonmul  33727  esplyind  33752  algextdeglem8  33902  zarcls  34052  xrmulc1cn  34108  xrge0iifcnv  34111  esumfsup  34248  esumpcvgval  34256  esumcvg  34264  esum2dlem  34270  issgon  34301  eulerpartgbij  34550  eulerpartlemgh  34556  ballotlemsima  34694  bnj1366  35005  bnj553  35074  bnj964  35119  fineqvnttrclse  35302  cusgredgex  35338  revwlk  35341  loop1cycl  35353  subfacp1lem3  35398  subfacp1lem5  35400  erdszelem9  35415  prv1n  35647  ply1divalg3  35858  quad3  35886  br6  35973  elintfv  35981  dfon2lem5  36001  dfon2lem8  36004  brbigcup  36112  dfbigcup2  36113  elfix  36117  ellimits  36124  snelsingles  36136  dfiota3  36137  imageval  36144  brapply  36152  lemsuccf  36155  dfsuccf2  36157  funpartlem  36158  brfullfun  36164  dfrecs2  36166  dfrdg4  36167  altopthbg  36184  altopthc  36187  altopthd  36188  altopelaltxp  36192  brsegle  36324  outsideofrflx  36343  elicc3  36533  nn0prpw  36539  opnregcld  36546  cldregopn  36547  fneval  36568  topfneec  36571  knoppndvlem9  36742  bj-elgab  37187  bj-gabima  37188  bj-elsngl  37216  bj-snglc  37217  bj-projval  37244  bj-disj2r  37276  bj-restreg  37352  bj-0int  37354  copsex2gd  37393  copsex2b  37395  bj-inftyexpitaudisj  37460  bj-inftyexpidisj  37465  bj-bary1lem1  37566  topdifinffinlem  37602  topdifinfeq  37605  fvineqsnf1  37665  curf  37849  uncf  37850  curunc  37853  unccur  37854  poimirlem2  37873  poimirlem16  37887  poimirlem17  37888  poimirlem19  37890  poimirlem20  37891  poimirlem27  37898  mblfinlem2  37909  mbfresfi  37917  itg2addnclem2  37923  ftc1anclem3  37946  fdc  37996  heibor1  38061  opidonOLD  38103  0rngo  38278  smprngopr  38303  isfldidl  38319  isfldidl2  38320  eqbrb  38490  eqelb  38492  ideq2  38564  relcnveq  38579  n0elqs  38583  disjressuc2  38662  dfsucmap3  38714  dfsucmap4  38716  dmsucmap  38719  preuniqval  38747  elrelscnveq  38879  qseq  38984  disjdmqscossss  39157  lcvnbtwn3  39404  lcvexchlem1  39410  lsatnem0  39421  opcon1b  39574  omllaw2N  39620  cmtbr2N  39629  leatb  39668  cvlsupr2  39719  glbconxN  39754  islln3  39886  llnexatN  39897  islpln3  39909  lplnexatN  39939  islvol3  39952  dalem-cly  40047  isline4N  40153  2llnma3r  40164  poml4N  40329  4atex2  40453  4atex2-0bOLDN  40455  cdlemefrs29bpre0  40772  cdlemftr3  40941  cdlemb3  40982  cdlemg17h  41044  cdlemg17pq  41048  cdlemg19  41060  cdlemg21  41062  tendoex  41351  dva1dim  41361  dihglb2  41718  doch11  41749  dochsordN  41750  lcfrlem9  41926  hlhillcs  42334  lcmineqlem4  42402  aks6d1c7lem2  42551  aks5lem3a  42559  aks5lem6  42562  unitscyglem2  42566  unitscyglem3  42567  addsubeq4com  42650  ef11d  42709  fimgmcyclem  42903  fsuppind  42948  elrfirn  43052  isnacs2  43063  isnacs3  43067  fiphp3d  43176  wopprc  43387  islnm2  43435  kercvrlsm  43440  fgraphopab  43560  tfsconcatlem  43693  tfsconcatrn  43699  tfsconcat0i  43702  tfsconcat0b  43703  tfsconcatrev  43705  oaun3lem1  43731  oadif1lem  43736  oadif1  43737  rp-fakeuninass  43872  snen1g  43880  iscard4  43889  sqrtcval  43997  frege124d  44117  frege129d  44119  frege92  44311  dffrege99  44318  clsk3nimkb  44396  clsk1indlem4  44400  clsk1indlem1  44401  ntrclsiso  44423  ntrclsk3  44426  ntrclsk13  44427  ntrneik4w  44456  extoimad  44520  int-sqdefd  44537  int-sqgeq0d  44542  radcnvrat  44670  bcc0  44696  opelopab4  44907  eqsbc2VD  45195  fzisoeu  45662  iuneqfzuz  45694  supxrleubrnmptf  45809  rexanuz2nf  45850  fsummulc1f  45931  fsumiunss  45935  fmul01lt1lem2  45945  sumnnodd  45990  fnlimfvre2  46035  limsupreuz  46095  limsupvaluz2  46096  liminfvalxr  46141  icccncfext  46245  cncfiooicc  46252  cncfioobdlem  46254  dvmptmulf  46295  dvmptfprodlem  46302  volioc  46330  itgioocnicc  46335  fourierdlem12  46477  fourierdlem20  46485  fourierdlem25  46490  fourierdlem33  46498  fourierdlem42  46507  fourierdlem52  46516  fourierdlem54  46518  fourierdlem57  46521  fourierdlem58  46522  fourierdlem59  46523  fourierdlem63  46527  fourierdlem65  46529  fourierdlem68  46532  fourierdlem73  46537  fourierdlem74  46538  fourierdlem75  46539  fourierdlem80  46544  fourierdlem81  46545  rrndistlt  46648  sge0ltfirpmpt2  46784  sge0pnfmpt  46803  hoidmv1le  46952  hoidmvle  46958  vonioolem2  47039  smflimlem3  47131  chnsubseqwl  47237  lambert0  47247  lamberte  47248  euabsneu  47388  funressnfv  47403  aiotaval  47455  reuf1odnf  47467  reuf1od  47468  afvpcfv0  47506  dfafn5a  47520  afvelrnb  47523  afvelrnb0  47524  dfaimafn2  47526  dfatsnafv2  47612  dfatdmfcoafv2  47614  f1oresf1o2  47651  ceilbi  47693  minusmodnep2tmod  47713  0nelsetpreimafv  47750  fargshiftfo  47802  sprsymrelf1  47856  reupr  47882  fmtnorec2lem  47902  fmtnoprmfac1  47925  fmtnoprmfac2  47927  sfprmdvdsmersenne  47963  lighneallem2  47966  dfeven2  48009  dfodd3  48010  odd2np1ALTV  48034  even3prm2  48079  fppr2odd  48091  nnsum3primesgbe  48152  nnsum3primesle9  48154  clnbgrsym  48198  dfvopnbgr2  48213  isuspgrim0  48254  isuspgrimlem  48255  dfgric2  48275  grtriprop  48301  uspgrlimlem3  48350  gpgvtxedg1  48424  pgnbgreunbgrlem2lem1  48474  pgnbgreunbgrlem2lem2  48475  0nodd  48530  2nodd  48532  lmod0rng  48589  rngcinvALTV  48636  ringcinvALTV  48670  lcoel0  48788  lindslinindimp2lem4  48821  ldepspr  48833  lincresunit3  48841  nn0sumshdiglemB  48980  nn0sumshdiglem1  48981  rrx2pnedifcoorneorr  49077  eenglngeehlnmlem1  49097  eenglngeehlnmlem2  49098  rrx2linest  49102  rrx2linest2  49104  rrxsphere  49108  line2ylem  49111  line2x  49114  itscnhlc0xyqsol  49125  itschlc0xyqsol1  49126  itsclinecirc0b  49134  2itscp  49141  inlinecirc02plem  49146  brab2dd  49187  uptr2  49580