Theorem eqeq1 2731

Description: Equality implies equivalence of equalities. (Contributed by NM, 26-May-1993.) (Proof shortened by Wolf Lammen, 19-Nov-2019.)

Assertion

Ref	Expression
eqeq1	⊢ (𝐴 = 𝐵 → (𝐴 = 𝐶 ↔ 𝐵 = 𝐶))

Proof of Theorem eqeq1

Step	Hyp	Ref	Expression
1		id 22	. 2 ⊢ (𝐴 = 𝐵 → 𝐴 = 𝐵)
2	1	eqeq1d 2729	1 ⊢ (𝐴 = 𝐵 → (𝐴 = 𝐶 ↔ 𝐵 = 𝐶))

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1534

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-9 2109  ax-ext 2698

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1775  df-cleq 2719

This theorem is referenced by:  eqeq1i  2732  eqeq12OLD  2746  eqtr  2750  eqtr2  2751  eqsb1  2854  clelab  2874  clelabOLD  2875  issetft  3483  cgsex4gOLD  3517  sbhypfOLD  3535  rexraleqim  3631  eqvincf  3634  pm13.183  3652  moeq  3700  mob  3710  euind  3717  reu2eqd  3729  reuind  3746  eqsbc1  3823  sbceqal  3839  csbhypf  3918  uniiunlem  4080  snjust  4623  elsng  4638  elprg  4645  reusngf  4672  rexreusng  4679  reuprg0  4702  rabrsn  4724  preq12bg  4850  intab  4976  uniintsn  4985  dfiun2g  5027  dfiin2g  5029  disji2  5124  disjprgw  5137  disjprg  5138  unopab  5224  eusv1  5385  reusv2lem2  5393  reusv3  5399  opthg  5473  copsexgw  5486  copsexg  5487  propeqop  5503  euotd  5509  otiunsndisj  5516  elopabw  5522  solin  5609  elxpi  5694  opbrop  5769  relop  5847  ideqg  5848  dmopab2rex  5914  elrnmpt  5952  elrnmpt1  5954  elrnmptg  5955  restidsing  6050  somin1  6133  cnveqb  6194  reu3op  6290  reuop  6291  ordequn  6466  iotaval2  6510  funopg  6581  f0rn0  6776  fvelrnb  6953  fvmptg  6997  fndmin  7048  eldmrexrn  7095  foelrn  7111  foelrnf  7112  foco2  7113  fmptco  7132  funopsn  7151  funsndifnop  7154  fmptsng  7171  fmptsnd  7172  tpres  7207  eufnfv  7235  elabrex  7246  elabrexg  7247  abrexco  7248  f1veqaeq  7261  fpropnf1  7271  nf1const  7307  isosolem  7349  f1oiso  7353  eusvobj2  7406  oprabidw  7445  oprabid  7446  f1opr  7470  oprabv  7474  0mpo0  7497  mpofunOLD  7539  elrnmpog  7550  elrnmpo  7551  elrnmpores  7553  ralrnmpo  7554  ov3  7578  ov6g  7579  ovelrn  7591  caovcang  7616  caovcan  7619  uniuni  7758  orduninsuc  7841  funcnvuni  7933  fiunlem  7939  fiun  7940  f1iun  7941  f1oweALT  7970  opiota  8057  eloprabi  8061  frxp  8125  funsssuppss  8188  dftpos4  8244  tz7.44-2  8421  tz7.44-3  8422  oev  8528  oalimcl  8574  omlimcl  8592  odi  8593  omeu  8599  oeeui  8616  nneob  8670  omopth  8676  eldifsucnn  8678  elqsg  8778  qsdisj  8804  qsel  8806  brecop  8820  eroveu  8822  erovlem  8823  elixpsn  8947  ixpsnf1o  8948  boxcutc  8951  2dom  9046  fundmen  9047  xpf1o  9155  nneneq  9225  nneneqOLD  9237  fofinf1o  9343  elfi  9428  elfiun  9445  dffi3  9446  brwdom  9582  brwdom3  9597  unwdomg  9599  xpwdomg  9600  noinfep  9675  cantnfp1lem1  9693  cantnfp1lem3  9695  cantnflem1  9704  ssttrcl  9730  ttrclselem2  9741  scott0  9901  updjudhcoinrg  9948  updjud  9949  carden2a  9981  cardiun  9997  pm54.43lem  10015  alephval3  10125  dfac5lem3  10140  dfac5lem4  10141  dfac2b  10145  kmlem9  10173  kmlem12  10176  cardcf  10267  cfeq0  10271  cfsuc  10272  cff1  10273  cflim2  10278  cfss  10280  isfin5  10314  fin1a2lem11  10425  fin1a2lem13  10427  brdom7disj  10546  brdom6disj  10547  canthp1lem2  10668  canthp1  10669  tskuni  10798  gruina  10833  genpv  11014  genpelv  11015  addsrmo  11088  mulsrmo  11089  ltsosr  11109  ltresr  11155  axcnre  11179  axpre-lttri  11180  ltordlem  11761  ltord1  11762  fimaxre3  12182  supaddc  12203  supadd  12204  supmul1  12205  supmullem1  12206  supmullem2  12207  supmul  12208  creur  12228  creui  12229  nn1m1nn  12255  elz  12582  nn0ind-raph  12684  xnegeq  13210  xmullem2  13268  xmulasslem  13288  fleqceilz  13843  fseqsupubi  13967  sqeqor  14203  nn0opth2  14255  hash1snb  14402  hash2prde  14455  prprrab  14458  hash2pwpr  14461  fi1uzind  14482  wrd2ind  14697  cshfn  14764  cshf1  14784  2cshwcshw  14800  scshwfzeqfzo  14801  pfx2  14922  s3iunsndisj  14939  relexpsucnnr  14996  relexprelg  15009  rtrclreclem3  15031  shftfval  15041  sgnval  15059  01sqrexlem6  15218  reusq0  15433  summo  15687  fsum  15690  telfsumo  15772  infcvgaux1i  15827  infcvgaux2i  15828  mertenslem1  15854  mertenslem2  15855  mertens  15856  prodmo  15904  fprod  15909  ruclem12  16209  mod2eq1n2dvds  16315  divalg  16371  ndvdssub  16377  sadcp1  16421  smupp1  16446  gcdval  16462  bezoutlem1  16506  bezoutlem3  16508  bezoutlem4  16509  bezout  16510  lcmval  16554  coprmgcdb  16611  coprmdvds1  16614  divgcdcoprmex  16628  dvdsprime  16649  nprm  16650  dvdsprm  16665  coprm  16673  qnumval  16700  qdenval  16701  m1dvdsndvds  16758  reumodprminv  16764  pcval  16804  pceu  16806  pczpre  16807  pcdiv  16812  4sqlem2  16909  4sqlem4  16912  4sqlem12  16916  4sq  16924  vdwapval  16933  vdwapun  16934  vdwlem6  16946  cshwrepswhash1  17063  acsfn  17630  initoid  17981  termoid  17982  cat1lem  18076  posi  18300  gsumval2a  18636  smndex2dnrinv  18858  mgm2nsgrplem2  18862  mgm2nsgrplem3  18863  sgrp2nmndlem5  18872  mgmnsgrpex  18874  sgrpnmndex  18875  cyccom  19149  ghmf1  19191  conjnmzb  19198  orbsta  19255  symgextfv  19364  symgextfo  19368  symgfixfo  19385  pmtrprfval  19433  pmtrprfvalrn  19434  psgneu  19452  psgnval  19453  psgnvali  19454  psgnvalii  19455  odfval  19478  odval  19480  dfod2  19510  submod  19515  isslw  19554  sylow2alem1  19563  sylow3lem2  19574  lsmelvalm  19597  lsmdisj2  19628  efgrelexlemb  19696  frgpup3lem  19723  cyggeninv  19829  gsumval3eu  19850  gsumval3lem2  19852  gsummpt1n0  19911  nn0gsumfz  19930  dprddisj2  19987  dpjrid  20010  pgpfac1lem3  20025  abveq0  20695  abvtrivd  20709  lss1d  20836  lspsn  20875  lspsnel  20876  lspprel  20968  rrgeq0i  21225  domneq0  21233  prmirredlem  21385  znf1o  21472  znfld  21481  znunit  21484  cygznlem3  21490  psgndif  21521  ipeq0  21557  obsip  21642  frlmphl  21702  uvcvval  21707  ellspd  21723  psrlidm  21892  psrridm  21893  mvrval2  21912  mvrf1  21915  mplmonmul  21961  evlslem3  22013  mhpsclcl  22058  psdmplcl  22073  psdmul  22077  coe1tm  22179  coe1tmfv2  22181  cply1coe0  22207  cply1coe0bi  22208  gsummoncoe1  22214  mamufacex  22278  mat1comp  22329  mat1dimelbas  22360  mat1dimid  22363  scmatel  22394  scmateALT  22401  mavmulsolcl  22440  marrepeval  22452  marepveval  22457  mdetunilem8  22508  maducoeval2  22529  madugsum  22532  minmar1eval  22538  symgmatr01lem  22542  symgmatr01  22543  gsummatr01lem3  22546  gsummatr01lem4  22547  gsummatr01  22548  m2cpm  22630  m2cpminvid2lem  22643  decpmatid  22659  monmatcollpw  22668  pmatcollpw3fi1lem1  22675  mp2pm2mplem4  22698  fvmptnn04ifc  22741  chfacffsupp  22745  chfacfscmul0  22747  chfacfscmulgsum  22749  chfacfpmmul0  22751  chfacfpmmulgsum  22753  cpmadumatpoly  22772  cayleyhamilton  22779  cayleyhamiltonALT  22780  istopon  22801  toponsspwpw  22811  fctop  22894  cctop  22896  ppttop  22897  pptbas  22898  epttop  22899  t0sep  23215  t1sep2  23260  cmpsublem  23290  cmpsub  23291  unisngl  23418  txuni2  23456  elpt  23463  ptbasfi  23472  xkoopn  23480  ptpjopn  23503  ptclsg  23506  dfac14lem  23508  ptcnp  23513  ptrescn  23530  tx1stc  23541  qtopeu  23607  kqt0lem  23627  isr0  23628  hauspwpwf1  23878  xmeteq0  24231  imasf1oxmet  24268  comet  24409  stdbdxmet  24411  met2ndci  24418  prdsxmslem2  24425  nrmmetd  24470  tngngp  24558  tngngp3  24560  xrsxmet  24712  iccpnfcnv  24856  iccpnfhmeo  24857  cnheibor  24868  elovolm  25391  ovolgelb  25396  ovolicc1  25432  ovolicc  25439  ioorval  25490  uniioombllem6  25504  dyadmax  25514  dyadmbl  25516  i1fadd  25611  i1fmul  25612  itg1addlem3  25614  i1fmulc  25620  itg2l  25646  itg2leub  25651  limcmpt  25799  limcco  25809  dvcobr  25864  dvcobrOLD  25865  deg1ldg  26015  ig1pval  26097  elply  26116  elply2  26117  coeval  26144  coe1termlem  26179  coe1term  26180  quotval  26214  plydivlem4  26218  plydivex  26219  vieta1  26234  aannenlem2  26251  aalioulem2  26255  abelthlem9  26364  logtayllem  26580  logtayl  26581  isosctrlem2  26738  leibpilem2  26860  rlimcnp2  26885  efrlim  26888  efrlimOLD  26889  mpodvdsmulf1o  27113  dvdsmulf1o  27115  perfectlem2  27150  lgsfval  27222  lgsval2lem  27227  lgsqrmodndvds  27273  lgsdchrval  27274  gausslemma2dlem0i  27284  2lgslem1b  27312  2lgslem3  27324  2sqlem2  27338  2sqlem8  27346  2sqlem9  27347  2sqlem11  27349  addsq2reu  27360  dchrisum0flblem1  27428  padicval  27537  padicabv  27550  ostth1  27553  sltval2  27576  sltintdifex  27581  sltres  27582  nolt02o  27615  madef  27770  addsval2  27867  addsproplem2  27874  addsproplem4  27876  addsproplem5  27877  addsproplem6  27878  addsprop  27880  addscut  27882  sleadd1  27893  addsuniflem  27905  addsunif  27906  addsasslem1  27907  addsasslem2  27908  negsprop  27934  negsid  27940  mulsval2lem  27997  mulsproplem9  28011  mulsproplem12  28014  mulsprop  28017  ssltmul1  28034  ssltmul2  28035  mulsuniflem  28036  addsdilem1  28038  addsdilem2  28039  mulsasslem1  28050  mulsasslem2  28051  mulsunif2  28057  precsexlemcbv  28091  precsexlem9  28100  precsexlem11  28102  recut  28211  0reno  28212  renegscl  28213  readdscl  28214  remulscllem1  28215  remulscl  28217  axtgcgrid  28254  axtgbtwnid  28257  islmib  28578  inaghl  28636  axpaschlem  28738  axlowdimlem15  28754  axlowdim  28759  upgredg2vtx  28941  edglnl  28943  umgredgnlp  28947  usgredg2vtxeuALT  29022  uspgredg2v  29024  ushgredgedgloop  29031  nbusgredgeu  29166  cusgrfilem2  29257  cusgrfi  29259  vtxdushgrfvedg  29291  1loopgrvd2  29304  rusgr1vtxlem  29388  wlkeq  29435  wlkp1lem8  29481  upgrwlkdvdelem  29537  crctcshwlkn0lem6  29613  wlknwwlksnbij  29686  rusgrnumwwlkl1  29766  clwlkclwwlklem2a1  29789  clwwlknscsh  29859  eleclclwwlkn  29873  hashecclwwlkn1  29874  umgrhashecclwwlk  29875  clwwlknon1sn  29897  frgr3vlem1  30070  3vfriswmgrlem  30074  frgrncvvdeqlem3  30098  wlkl0  30164  frgrreggt1  30190  nvz  30466  nmosetn0  30562  nmoolb  30568  nmoubi  30569  nmlno0lem  30590  nmlno0i  30591  hvsubeq0  30865  hvaddcan  30867  normsub0  30933  norm1exi  31047  pjhval  31194  omlsii  31200  omlsi  31201  pjoml  31233  h1de2ci  31353  spansneleq  31367  h1datomi  31378  h1datom  31379  spansncv  31450  5oalem6  31456  pj11  31511  nmopsetn0  31662  nmfnsetn0  31675  nmoplb  31704  nmopub  31705  nmfnlb  31721  nmfnleub  31722  nmlnop0iALT  31792  nmlnop0  31795  lnopeq  31806  nmopun  31811  nmcexi  31823  branmfn  31902  pjnmopi  31945  pj3i  32005  atss  32143  atom1d  32150  chirred  32192  cdj3lem2  32232  eqelbid  32259  elabreximd  32291  disjxpin  32363  disjunsn  32369  br8d  32383  fmptcof2  32426  psgnfzto1stlem  32799  sgnsval  32860  domnlcan  32914  linds2eq  33036  elrspunsn  33080  mxidlmax  33114  lbsdiflsp0  33256  fedgmullem1  33259  fedgmullem2  33260  madjusmdetlem2  33365  madjusmdet  33368  zarclssn  33410  xrge0iifcnv  33470  xrge0iifcv  33471  xrge0iifhom  33474  xrge0tmd  33482  xrge0tmdALT  33483  esumc  33606  sgn3da  34097  sgnmul  34098  sgnnbi  34101  sgnpbi  34102  sgn0bi  34103  plymulx0  34115  signspval  34120  tgoldbachgt  34231  bnj1468  34413  f1resfz0f1d  34659  acycgrcycl  34693  sconnpi1  34785  cvmlift3lem2  34866  satfv0  34904  satfv1  34909  satfbrsuc  34912  satfrnmapom  34916  satfv0fun  34917  satf0op  34923  sat1el2xp  34925  fmlafvel  34931  fmla1  34933  isfmlasuc  34934  fmlaomn0  34936  gonan0  34938  goaln0  34939  gonar  34941  goalr  34943  fmla0disjsuc  34944  fmlasucdisj  34945  satffunlem1lem1  34948  satffunlem2lem1  34950  dmopab3rexdif  34951  satfv0fvfmla0  34959  sategoelfvb  34965  ex-sategoelel  34967  satfv1fvfmla1  34969  2goelgoanfmla1  34970  ex-sategoelelomsuc  34972  ex-sategoelel12  34973  prv1n  34977  br8  35286  br6  35287  br4  35288  rdgprc0  35325  dfrdg2  35327  dfbigcup2  35431  elsingles  35450  dfiota3  35455  brimageg  35459  brdomaing  35467  brrangeg  35468  dfrdg4  35483  elaltxp  35507  funtransport  35563  fvtransport  35564  brsegle  35640  funray  35672  fvray  35673  funline  35674  fvline  35676  ellines  35684  linethru  35685  rankeq1o  35703  subtr  35734  subtr2  35735  nn0prpw  35743  bj-elabd2ALT  36339  bj-gabss  36349  bj-imafv  36666  topdifinffinlem  36762  topdifinffin  36763  topdifinfeq  36765  finxpreclem2  36805  finxpreclem3  36808  fvineqsnf1  36825  fvineqsneu  36826  wl-issetft  36984  fin2so  37015  ptrest  37027  poimirlem25  37053  poimirlem26  37054  poimirlem27  37055  poimirlem28  37056  poimirlem31  37059  poimirlem32  37060  heicant  37063  mblfinlem2  37066  mblfinlem3  37067  mblfinlem4  37068  ismblfin  37069  itg2addnclem  37079  itg2addnclem3  37081  itg2addnc  37082  ftc1anc  37109  unirep  37122  sdclem2  37150  sdclem1  37151  sdc  37152  fdc  37153  isbnd  37188  heibor1lem  37217  heiborlem4  37222  heiborlem6  37224  heiborlem10  37228  ismgmOLD  37258  maxidlmax  37451  prnc  37475  isfldidl  37476  dmnnzd  37483  disjressuc2  37797  qsdisjALTV  38024  eqvrelqsel  38025  riotasvd  38365  lshpdisj  38396  lsat0cv  38442  lcvexchlem4  38446  lcvexchlem5  38447  lshpkrlem1  38519  lshpkrlem2  38520  lshpkrlem3  38521  lshpkrcl  38525  islshpkrN  38529  atnle  38726  glbconxN  38788  isline  39149  ispointN  39152  pmapglbx  39179  ispsubcl2N  39357  lhp2atnle  39443  cdleme43fsv1snlem  39830  cdleme40v  39879  cdlemkid5  40345  cdlemkid  40346  dvhb1dimN  40396  dib1dim  40575  dicopelval  40587  dicelval1sta  40597  diclspsn  40604  dihvalcqpre  40645  dihglblem2aN  40703  dihglblem2N  40704  dih1dimatlem  40739  dihpN  40746  dochfl1  40886  lcfl7N  40911  lcf1o  40961  hvmapvalvalN  41171  hdmapval2lem  41241  aks6d1c1  41520  sticksstones10  41559  sticksstones12a  41561  metakunt3  41579  metakunt4  41580  metakunt6  41582  metakunt7  41583  metakunt8  41584  metakunt10  41586  metakunt11  41587  metakunt12  41588  metakunt20  41596  metakunt21  41597  metakunt22  41598  metakunt24  41600  sn-iotalem  41629  f1o2d2  41644  evlsbagval  41721  selvvvval  41740  fsuppind  41745  sn-negex12  41893  elrfi  42036  nacsfg  42047  mzpcompact2lem  42093  eldioph2b  42105  eldioph3  42108  eldiophss  42116  diophrex  42117  elnn0rabdioph  42145  rencldnfilem  42162  elpell1qr  42189  elpell14qr  42191  elpell1234qr  42193  jm2.27  42351  rmydioph  42357  expdiophlem2  42365  wepwsolem  42388  aomclem6  42405  lnr2i  42462  lpirlnr  42463  hbtlem2  42470  hbtlem4  42472  hbtlem5  42474  rngunsnply  42519  flcidc  42520  onsucelab  42615  limnsuc  42617  nnoeomeqom  42664  cantnfresb  42676  tfsconcatfv2  42692  tfsconcatb0  42696  oaun3lem1  42726  oadif1lem  42731  oadif1  42732  clcnvlem  42976  brtrclfv2  43080  frege55lem1c  43269  frege104  43320  clsk1indlem0  43394  clsk1indlem2  43395  clsk1indlem3  43396  clsk1indlem4  43397  clsk1indlem1  43398  pm13.192  43770  equncomVD  44230  csbingVD  44246  csbsngVD  44255  csbfv12gALTVD  44261  relopabVD  44263  refsum2cnlem1  44322  elrnmptf  44477  upbdrech  44610  ssfiunibd  44614  iccshift  44826  iooshift  44830  fsumf1of  44885  limcperiod  44939  climinf2mpt  45025  climinfmpt  45026  cncfshiftioo  45203  itgiccshift  45291  itgperiod  45292  stoweidlem46  45357  fourierdlem29  45447  fourierdlem37  45455  fourierdlem48  45465  fourierdlem51  45468  fourierdlem54  45471  fourierdlem62  45479  fourierdlem79  45496  fourierdlem81  45498  fourierdlem82  45499  fourierdlem92  45509  fourierdlem96  45513  fourierdlem97  45514  fourierdlem98  45515  fourierdlem99  45516  fourierdlem103  45520  fourierdlem104  45521  fourierdlem105  45522  fourierdlem108  45525  fourierdlem110  45527  fourierdlem112  45529  etransclem1  45546  etransclem5  45550  etransclem17  45562  etransclem32  45577  etransclem41  45586  sge0f1o  45693  sge0resplit  45717  sge0fodjrnlem  45727  nnfoctbdjlem  45766  nnfoctbdj  45767  ovnval  45852  ovnlecvr  45869  ovnpnfelsup  45870  ovn0lem  45876  hoidmvval  45888  hoidmvlelem1  45906  ovnhoilem1  45912  ovnhoi  45914  ovnlecvr2  45921  hoidifhspval3  45930  hspmbllem2  45938  hoimbl  45942  ovnsubadd2  45957  ovolval5lem2  45964  ovolval5lem3  45965  ovolval5  45966  ovnovol  45970  fsetsnf  46356  fsetsnfo  46358  fcoresf1  46374  aiotaval  46398  euoreqb  46412  afv0fv0  46452  afvfv0bi  46455  afvelrnb  46466  afvelrnb0  46467  afv20defat  46535  otiunsndisjX  46582  fun2dmnopgexmpl  46587  2ffzoeq  46631  elsetpreimafvb  46647  imasetpreimafvbijlemfo  46668  fargshiftf1  46704  fargshiftfo  46705  ichnreuop  46735  ichreuopeq  46736  elsprel  46738  spr0nelg  46739  sprel  46747  prelspr  46749  sprsymrelf1lem  46754  sprsymrelfolem2  46756  paireqne  46774  prprelb  46779  prprelprb  46780  reupr  46785  reuopreuprim  46789  fmtnoprmfac1lem  46827  fmtnofac2  46832  m1expevenALTV  46910  odd2np1ALTV  46937  opoeALTV  46946  opeoALTV  46947  perfectALTVlem2  46985  isgbe  47014  isgbow  47015  isgbo  47016  sbgoldbalt  47044  sgoldbeven3prm  47046  mogoldbb  47048  nnsum3primesgbe  47055  nnsum3primesle9  47057  nnsum4primesodd  47059  nnsum4primesoddALTV  47060  isuspgrim0  47093  isuspgrimlem  47095  uspgrsprf1  47132  uspgrsprfo  47133  0nodd  47155  1odd  47156  2nodd  47157  0even  47222  1neven  47223  2even  47224  2zlidl  47225  2zrngamgm  47230  2zrngagrp  47234  2zrngmmgm  47237  2zrngnmrid  47241  suppmptcfin  47366  lcoval  47403  linc0scn0  47414  linc1  47416  el0ldep  47457  snlindsntor  47462  blenval  47567  nn0sumshdiglemB  47616  itcoval1  47659  mo0  47807  isthincd2lem1  47956