Theorem eqeq1 2734

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 2732	1 ⊢ (𝐴 = 𝐵 → (𝐴 = 𝐶 ↔ 𝐵 = 𝐶))

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

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 1911  ax-6 1969  ax-7 2009  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1780  df-cleq 2722

This theorem is referenced by:  eqeq1i  2735  eqeq12OLD  2749  eqtr  2753  eqtr2  2754  eqsb1  2857  clelab  2877  clelabOLD  2878  issetft  3486  cgsex4gOLD  3520  sbhypfOLD  3538  rexraleqim  3636  eqvincf  3639  pm13.183  3657  moeq  3704  mob  3714  euind  3721  reu2eqd  3733  reuind  3750  eqsbc1  3827  sbceqal  3844  csbhypf  3923  uniiunlem  4085  snjust  4628  elsng  4643  elprg  4650  reusngf  4677  rexreusng  4684  reuprg0  4707  rabrsn  4729  preq12bg  4855  intab  4983  uniintsn  4992  dfiun2g  5034  dfiin2g  5036  disji2  5131  disjprgw  5144  disjprg  5145  unopab  5231  eusv1  5390  reusv2lem2  5398  reusv3  5404  opthg  5478  copsexgw  5491  copsexg  5492  propeqop  5508  euotd  5514  otiunsndisj  5521  elopabw  5527  solin  5614  elxpi  5699  opbrop  5774  relop  5851  ideqg  5852  dmopab2rex  5918  elrnmpt  5956  elrnmpt1  5958  elrnmptg  5959  restidsing  6053  somin1  6135  cnveqb  6196  reu3op  6292  reuop  6293  ordequn  6468  iotaval2  6512  funopg  6583  f0rn0  6777  fvelrnb  6953  fvmptg  6997  fndmin  7047  eldmrexrn  7093  foelrn  7109  foelrnf  7110  foco2  7111  fmptco  7130  funopsn  7149  funsndifnop  7152  fmptsng  7169  fmptsnd  7170  tpres  7205  eufnfv  7234  elabrex  7245  elabrexg  7246  abrexco  7247  f1veqaeq  7260  fpropnf1  7270  nf1const  7306  isosolem  7348  f1oiso  7352  eusvobj2  7405  oprabidw  7444  oprabid  7445  f1opr  7469  oprabv  7473  0mpo0  7496  mpofunOLD  7537  elrnmpog  7548  elrnmpo  7549  elrnmpores  7550  ralrnmpo  7551  ov3  7574  ov6g  7575  ovelrn  7587  caovcang  7612  caovcan  7615  uniuni  7753  orduninsuc  7836  funcnvuni  7926  fiunlem  7932  fiun  7933  f1iun  7934  f1oweALT  7963  opiota  8049  eloprabi  8053  frxp  8116  funsssuppss  8179  dftpos4  8234  tz7.44-2  8411  tz7.44-3  8412  oev  8518  oalimcl  8564  omlimcl  8582  odi  8583  omeu  8589  oeeui  8606  nneob  8659  omopth  8665  eldifsucnn  8667  elqsg  8766  qsdisj  8792  qsel  8794  brecop  8808  eroveu  8810  erovlem  8811  elixpsn  8935  ixpsnf1o  8936  boxcutc  8939  2dom  9034  fundmen  9035  xpf1o  9143  nneneq  9213  nneneqOLD  9225  fofinf1o  9331  elfi  9412  elfiun  9429  dffi3  9430  brwdom  9566  brwdom3  9581  unwdomg  9583  xpwdomg  9584  noinfep  9659  cantnfp1lem1  9677  cantnfp1lem3  9679  cantnflem1  9688  ssttrcl  9714  ttrclselem2  9725  scott0  9885  updjudhcoinrg  9932  updjud  9933  carden2a  9965  cardiun  9981  pm54.43lem  9999  alephval3  10109  dfac5lem3  10124  dfac5lem4  10125  dfac2b  10129  kmlem9  10157  kmlem12  10160  cardcf  10251  cfeq0  10255  cfsuc  10256  cff1  10257  cflim2  10262  cfss  10264  isfin5  10298  fin1a2lem11  10409  fin1a2lem13  10411  brdom7disj  10530  brdom6disj  10531  canthp1lem2  10652  canthp1  10653  tskuni  10782  gruina  10817  genpv  10998  genpelv  10999  addsrmo  11072  mulsrmo  11073  ltsosr  11093  ltresr  11139  axcnre  11163  axpre-lttri  11164  ltordlem  11745  ltord1  11746  fimaxre3  12166  supaddc  12187  supadd  12188  supmul1  12189  supmullem1  12190  supmullem2  12191  supmul  12192  creur  12212  creui  12213  nn1m1nn  12239  elz  12566  nn0ind-raph  12668  xnegeq  13192  xmullem2  13250  xmulasslem  13270  fleqceilz  13825  fseqsupubi  13949  sqeqor  14186  nn0opth2  14238  hash1snb  14385  hash2prde  14437  prprrab  14440  hash2pwpr  14443  fi1uzind  14464  wrd2ind  14679  cshfn  14746  cshf1  14766  2cshwcshw  14782  scshwfzeqfzo  14783  pfx2  14904  s3iunsndisj  14921  relexpsucnnr  14978  relexprelg  14991  rtrclreclem3  15013  shftfval  15023  sgnval  15041  01sqrexlem6  15200  reusq0  15415  summo  15669  fsum  15672  telfsumo  15754  infcvgaux1i  15809  infcvgaux2i  15810  mertenslem1  15836  mertenslem2  15837  mertens  15838  prodmo  15886  fprod  15891  ruclem12  16190  mod2eq1n2dvds  16296  divalg  16352  ndvdssub  16358  sadcp1  16402  smupp1  16427  gcdval  16443  bezoutlem1  16487  bezoutlem3  16489  bezoutlem4  16490  bezout  16491  lcmval  16535  coprmgcdb  16592  coprmdvds1  16595  divgcdcoprmex  16609  dvdsprime  16630  nprm  16631  dvdsprm  16646  coprm  16654  qnumval  16679  qdenval  16680  m1dvdsndvds  16737  reumodprminv  16743  pcval  16783  pceu  16785  pczpre  16786  pcdiv  16791  4sqlem2  16888  4sqlem4  16891  4sqlem12  16895  4sq  16903  vdwapval  16912  vdwapun  16913  vdwlem6  16925  cshwrepswhash1  17042  acsfn  17609  initoid  17957  termoid  17958  cat1lem  18052  posi  18276  gsumval2a  18612  smndex2dnrinv  18834  mgm2nsgrplem2  18838  mgm2nsgrplem3  18839  sgrp2nmndlem5  18848  mgmnsgrpex  18850  sgrpnmndex  18851  cyccom  19120  ghmf1  19162  conjnmzb  19169  orbsta  19220  symgextfv  19329  symgextfo  19333  symgfixfo  19350  pmtrprfval  19398  pmtrprfvalrn  19399  psgneu  19417  psgnval  19418  psgnvali  19419  psgnvalii  19420  odfval  19443  odval  19445  dfod2  19475  submod  19480  isslw  19519  sylow2alem1  19528  sylow3lem2  19539  lsmelvalm  19562  lsmdisj2  19593  efgrelexlemb  19661  frgpup3lem  19688  cyggeninv  19794  gsumval3eu  19815  gsumval3lem2  19817  gsummpt1n0  19876  nn0gsumfz  19895  dprddisj2  19952  dpjrid  19975  pgpfac1lem3  19990  abveq0  20579  abvtrivd  20593  lss1d  20720  lspsn  20759  lspsnel  20760  lspprel  20851  rrgeq0i  21107  domneq0  21115  prmirredlem  21245  znf1o  21328  znfld  21337  znunit  21340  cygznlem3  21346  psgndif  21376  ipeq0  21412  obsip  21497  frlmphl  21557  uvcvval  21562  ellspd  21578  psrlidm  21744  psrridm  21745  mvrval2  21763  mvrf1  21766  mplmonmul  21812  evlslem3  21864  mhpsclcl  21911  coe1tm  22017  coe1tmfv2  22019  cply1coe0  22045  cply1coe0bi  22046  gsummoncoe1  22050  mamufacex  22113  mat1comp  22164  mat1dimelbas  22195  mat1dimid  22198  scmatel  22229  scmateALT  22236  mavmulsolcl  22275  marrepeval  22287  marepveval  22292  mdetunilem8  22343  maducoeval2  22364  madugsum  22367  minmar1eval  22373  symgmatr01lem  22377  symgmatr01  22378  gsummatr01lem3  22381  gsummatr01lem4  22382  gsummatr01  22383  m2cpm  22465  m2cpminvid2lem  22478  decpmatid  22494  monmatcollpw  22503  pmatcollpw3fi1lem1  22510  mp2pm2mplem4  22533  fvmptnn04ifc  22576  chfacffsupp  22580  chfacfscmul0  22582  chfacfscmulgsum  22584  chfacfpmmul0  22586  chfacfpmmulgsum  22588  cpmadumatpoly  22607  cayleyhamilton  22614  cayleyhamiltonALT  22615  istopon  22636  toponsspwpw  22646  fctop  22729  cctop  22731  ppttop  22732  pptbas  22733  epttop  22734  t0sep  23050  t1sep2  23095  cmpsublem  23125  cmpsub  23126  unisngl  23253  txuni2  23291  elpt  23298  ptbasfi  23307  xkoopn  23315  ptpjopn  23338  ptclsg  23341  dfac14lem  23343  ptcnp  23348  ptrescn  23365  tx1stc  23376  qtopeu  23442  kqt0lem  23462  isr0  23463  hauspwpwf1  23713  xmeteq0  24066  imasf1oxmet  24103  comet  24244  stdbdxmet  24246  met2ndci  24253  prdsxmslem2  24260  nrmmetd  24305  tngngp  24393  tngngp3  24395  xrsxmet  24547  iccpnfcnv  24691  iccpnfhmeo  24692  cnheibor  24703  elovolm  25226  ovolgelb  25231  ovolicc1  25267  ovolicc  25274  ioorval  25325  uniioombllem6  25339  dyadmax  25349  dyadmbl  25351  i1fadd  25446  i1fmul  25447  itg1addlem3  25449  i1fmulc  25455  itg2l  25481  itg2leub  25486  limcmpt  25634  limcco  25644  dvcobr  25697  deg1ldg  25844  ig1pval  25924  elply  25943  elply2  25944  coeval  25971  coe1termlem  26006  coe1term  26007  quotval  26039  plydivlem4  26043  plydivex  26044  vieta1  26059  aannenlem2  26076  aalioulem2  26080  abelthlem9  26186  logtayllem  26401  logtayl  26402  isosctrlem2  26558  leibpilem2  26680  rlimcnp2  26705  efrlim  26708  dvdsmulf1o  26932  perfectlem2  26967  lgsfval  27039  lgsval2lem  27044  lgsqrmodndvds  27090  lgsdchrval  27091  gausslemma2dlem0i  27101  2lgslem1b  27129  2lgslem3  27141  2sqlem2  27155  2sqlem8  27163  2sqlem9  27164  2sqlem11  27166  addsq2reu  27177  dchrisum0flblem1  27245  padicval  27354  padicabv  27367  ostth1  27370  sltval2  27393  sltintdifex  27398  sltres  27399  nolt02o  27432  madef  27586  addsval2  27683  addsproplem2  27690  addsproplem4  27692  addsproplem5  27693  addsproplem6  27694  addsprop  27696  addscut  27698  sleadd1  27709  addsuniflem  27721  addsunif  27722  addsasslem1  27723  addsasslem2  27724  negsprop  27746  negsid  27752  mulsval2lem  27803  mulsproplem9  27817  mulsproplem12  27820  mulsprop  27823  ssltmul1  27839  ssltmul2  27840  mulsuniflem  27841  addsdilem1  27843  addsdilem2  27844  mulsasslem1  27855  mulsasslem2  27856  precsexlemcbv  27889  precsexlem9  27898  precsexlem11  27900  axtgcgrid  27979  axtgbtwnid  27982  islmib  28303  inaghl  28361  axpaschlem  28463  axlowdimlem15  28479  axlowdim  28484  upgredg2vtx  28666  edglnl  28668  umgredgnlp  28672  usgredg2vtxeuALT  28744  uspgredg2v  28746  ushgredgedgloop  28753  nbusgredgeu  28888  cusgrfilem2  28978  cusgrfi  28980  vtxdushgrfvedg  29012  1loopgrvd2  29025  rusgr1vtxlem  29109  wlkeq  29156  wlkp1lem8  29202  upgrwlkdvdelem  29258  crctcshwlkn0lem6  29334  wlknwwlksnbij  29407  rusgrnumwwlkl1  29487  clwlkclwwlklem2a1  29510  clwwlknscsh  29580  eleclclwwlkn  29594  hashecclwwlkn1  29595  umgrhashecclwwlk  29596  clwwlknon1sn  29618  frgr3vlem1  29791  3vfriswmgrlem  29795  frgrncvvdeqlem3  29819  wlkl0  29885  frgrreggt1  29911  nvz  30187  nmosetn0  30283  nmoolb  30289  nmoubi  30290  nmlno0lem  30311  nmlno0i  30312  hvsubeq0  30586  hvaddcan  30588  normsub0  30654  norm1exi  30768  pjhval  30915  omlsii  30921  omlsi  30922  pjoml  30954  h1de2ci  31074  spansneleq  31088  h1datomi  31099  h1datom  31100  spansncv  31171  5oalem6  31177  pj11  31232  nmopsetn0  31383  nmfnsetn0  31396  nmoplb  31425  nmopub  31426  nmfnlb  31442  nmfnleub  31443  nmlnop0iALT  31513  nmlnop0  31516  lnopeq  31527  nmopun  31532  nmcexi  31544  branmfn  31623  pjnmopi  31666  pj3i  31726  atss  31864  atom1d  31871  chirred  31913  cdj3lem2  31953  eqelbid  31980  elabreximd  32012  disjxpin  32084  disjunsn  32090  br8d  32104  fmptcof2  32147  psgnfzto1stlem  32527  sgnsval  32588  domnlcan  32644  linds2eq  32769  elrspunsn  32819  mxidlmax  32853  lbsdiflsp0  32997  fedgmullem1  33000  fedgmullem2  33001  madjusmdetlem2  33104  madjusmdet  33107  zarclssn  33149  xrge0iifcnv  33209  xrge0iifcv  33210  xrge0iifhom  33213  xrge0tmd  33221  xrge0tmdALT  33222  esumc  33345  sgn3da  33836  sgnmul  33837  sgnnbi  33840  sgnpbi  33841  sgn0bi  33842  plymulx0  33854  signspval  33859  tgoldbachgt  33971  bnj1468  34153  f1resfz0f1d  34399  acycgrcycl  34434  sconnpi1  34526  cvmlift3lem2  34607  satfv0  34645  satfv1  34650  satfbrsuc  34653  satfrnmapom  34657  satfv0fun  34658  satf0op  34664  sat1el2xp  34666  fmlafvel  34672  fmla1  34674  isfmlasuc  34675  fmlaomn0  34677  gonan0  34679  goaln0  34680  gonar  34682  goalr  34684  fmla0disjsuc  34685  fmlasucdisj  34686  satffunlem1lem1  34689  satffunlem2lem1  34691  dmopab3rexdif  34692  satfv0fvfmla0  34700  sategoelfvb  34706  ex-sategoelel  34708  satfv1fvfmla1  34710  2goelgoanfmla1  34711  ex-sategoelelomsuc  34713  ex-sategoelel12  34714  prv1n  34718  br8  35028  br6  35029  br4  35030  rdgprc0  35067  dfrdg2  35069  dfbigcup2  35173  elsingles  35192  dfiota3  35197  brimageg  35201  brdomaing  35209  brrangeg  35210  dfrdg4  35225  elaltxp  35249  funtransport  35305  fvtransport  35306  brsegle  35382  funray  35414  fvray  35415  funline  35416  fvline  35418  ellines  35426  linethru  35427  rankeq1o  35445  gg-dvcobr  35464  subtr  35504  subtr2  35505  nn0prpw  35513  bj-elabd2ALT  36110  bj-gabss  36120  bj-imafv  36437  topdifinffinlem  36533  topdifinffin  36534  topdifinfeq  36536  finxpreclem2  36576  finxpreclem3  36579  fvineqsnf1  36596  fvineqsneu  36597  wl-issetft  36749  fin2so  36780  ptrest  36792  poimirlem25  36818  poimirlem26  36819  poimirlem27  36820  poimirlem28  36821  poimirlem31  36824  poimirlem32  36825  heicant  36828  mblfinlem2  36831  mblfinlem3  36832  mblfinlem4  36833  ismblfin  36834  itg2addnclem  36844  itg2addnclem3  36846  itg2addnc  36847  ftc1anc  36874  unirep  36887  sdclem2  36915  sdclem1  36916  sdc  36917  fdc  36918  isbnd  36953  heibor1lem  36982  heiborlem4  36987  heiborlem6  36989  heiborlem10  36993  ismgmOLD  37023  maxidlmax  37216  prnc  37240  isfldidl  37241  dmnnzd  37248  disjressuc2  37563  qsdisjALTV  37790  eqvrelqsel  37791  riotasvd  38131  lshpdisj  38162  lsat0cv  38208  lcvexchlem4  38212  lcvexchlem5  38213  lshpkrlem1  38285  lshpkrlem2  38286  lshpkrlem3  38287  lshpkrcl  38291  islshpkrN  38295  atnle  38492  glbconxN  38554  isline  38915  ispointN  38918  pmapglbx  38945  ispsubcl2N  39123  lhp2atnle  39209  cdleme43fsv1snlem  39596  cdleme40v  39645  cdlemkid5  40111  cdlemkid  40112  dvhb1dimN  40162  dib1dim  40341  dicopelval  40353  dicelval1sta  40363  diclspsn  40370  dihvalcqpre  40411  dihglblem2aN  40469  dihglblem2N  40470  dih1dimatlem  40505  dihpN  40512  dochfl1  40652  lcfl7N  40677  lcf1o  40727  hvmapvalvalN  40937  hdmapval2lem  41007  sticksstones10  41279  sticksstones12a  41281  metakunt3  41295  metakunt4  41296  metakunt6  41298  metakunt7  41299  metakunt8  41300  metakunt10  41302  metakunt11  41303  metakunt12  41304  metakunt20  41312  metakunt21  41313  metakunt22  41314  metakunt24  41316  sn-iotalem  41346  f1o2d2  41363  evlsbagval  41442  selvvvval  41461  fsuppind  41466  sn-negex12  41593  elrfi  41736  nacsfg  41747  mzpcompact2lem  41793  eldioph2b  41805  eldioph3  41808  eldiophss  41816  diophrex  41817  elnn0rabdioph  41845  rencldnfilem  41862  elpell1qr  41889  elpell14qr  41891  elpell1234qr  41893  jm2.27  42051  rmydioph  42057  expdiophlem2  42065  wepwsolem  42088  aomclem6  42105  lnr2i  42162  lpirlnr  42163  hbtlem2  42170  hbtlem4  42172  hbtlem5  42174  rngunsnply  42219  flcidc  42220  onsucelab  42317  limnsuc  42319  nnoeomeqom  42366  cantnfresb  42378  tfsconcatfv2  42394  tfsconcatb0  42398  oaun3lem1  42428  oadif1lem  42433  oadif1  42434  clcnvlem  42678  brtrclfv2  42782  frege55lem1c  42971  frege104  43022  clsk1indlem0  43096  clsk1indlem2  43097  clsk1indlem3  43098  clsk1indlem4  43099  clsk1indlem1  43100  pm13.192  43473  equncomVD  43933  csbingVD  43949  csbsngVD  43958  csbfv12gALTVD  43964  relopabVD  43966  refsum2cnlem1  44025  elrnmptf  44180  upbdrech  44315  ssfiunibd  44319  iccshift  44531  iooshift  44535  fsumf1of  44590  limcperiod  44644  climinf2mpt  44730  climinfmpt  44731  cncfshiftioo  44908  itgiccshift  44996  itgperiod  44997  stoweidlem46  45062  fourierdlem29  45152  fourierdlem37  45160  fourierdlem48  45170  fourierdlem51  45173  fourierdlem54  45176  fourierdlem62  45184  fourierdlem79  45201  fourierdlem81  45203  fourierdlem82  45204  fourierdlem92  45214  fourierdlem96  45218  fourierdlem97  45219  fourierdlem98  45220  fourierdlem99  45221  fourierdlem103  45225  fourierdlem104  45226  fourierdlem105  45227  fourierdlem108  45230  fourierdlem110  45232  fourierdlem112  45234  etransclem1  45251  etransclem5  45255  etransclem17  45267  etransclem32  45282  etransclem41  45291  sge0f1o  45398  sge0resplit  45422  sge0fodjrnlem  45432  nnfoctbdjlem  45471  nnfoctbdj  45472  ovnval  45557  ovnlecvr  45574  ovnpnfelsup  45575  ovn0lem  45581  hoidmvval  45593  hoidmvlelem1  45611  ovnhoilem1  45617  ovnhoi  45619  ovnlecvr2  45626  hoidifhspval3  45635  hspmbllem2  45643  hoimbl  45647  ovnsubadd2  45662  ovolval5lem2  45669  ovolval5lem3  45670  ovolval5  45671  ovnovol  45675  fsetsnf  46061  fsetsnfo  46063  fcoresf1  46079  aiotaval  46103  euoreqb  46117  afv0fv0  46157  afvfv0bi  46160  afvelrnb  46171  afvelrnb0  46172  afv20defat  46240  otiunsndisjX  46287  fun2dmnopgexmpl  46292  2ffzoeq  46336  elsetpreimafvb  46352  imasetpreimafvbijlemfo  46373  fargshiftf1  46409  fargshiftfo  46410  ichnreuop  46440  ichreuopeq  46441  elsprel  46443  spr0nelg  46444  sprel  46452  prelspr  46454  sprsymrelf1lem  46459  sprsymrelfolem2  46461  paireqne  46479  prprelb  46484  prprelprb  46485  reupr  46490  reuopreuprim  46494  fmtnoprmfac1lem  46532  fmtnofac2  46537  m1expevenALTV  46615  odd2np1ALTV  46642  opoeALTV  46651  opeoALTV  46652  perfectALTVlem2  46690  isgbe  46719  isgbow  46720  isgbo  46721  sbgoldbalt  46749  sgoldbeven3prm  46751  mogoldbb  46753  nnsum3primesgbe  46760  nnsum3primesle9  46762  nnsum4primesodd  46764  nnsum4primesoddALTV  46765  isomuspgrlem1  46795  uspgrsprf1  46825  uspgrsprfo  46826  0nodd  46848  1odd  46849  2nodd  46850  0even  46919  1neven  46920  2even  46921  2zlidl  46922  2zrngamgm  46927  2zrngagrp  46931  2zrngmmgm  46934  2zrngnmrid  46938  suppmptcfin  47145  lcoval  47182  linc0scn0  47193  linc1  47195  el0ldep  47236  snlindsntor  47241  blenval  47346  nn0sumshdiglemB  47395  itcoval1  47438  mo0  47587  isthincd2lem1  47736