Theorem eqeq1 2741

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

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1543

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-9 2120  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1788  df-cleq 2729

This theorem is referenced by:  eqeq1i  2742  eqeq12OLD  2756  eqtr  2760  eqtr2  2761  eqsb3  2864  clelab  2880  clelabOLD  2881  issetf  3422  cgsex4g  3452  sbhypf  3467  vtoclgft  3468  rexraleqim  3554  eqvincf  3557  pm13.183  3575  moeq  3620  mob  3630  euind  3637  reu2eqd  3649  reuind  3666  eqsbc3  3743  sbceqal  3761  csbhypf  3840  uniiunlem  3999  snjust  4540  elsng  4555  elprg  4562  reusngf  4588  rexreusng  4595  reuprg0  4618  rabrsn  4640  preq12bg  4764  intab  4889  uniintsn  4898  dfiin2g  4941  disji2  5035  disjprgw  5048  disjprg  5049  unopab  5134  eusv1  5284  reusv2lem2  5292  reusv3  5298  opthg  5361  copsexgw  5373  copsexg  5374  propeqop  5390  euotd  5396  otiunsndisj  5403  elopab  5408  solin  5493  elxpi  5573  opbrop  5645  relop  5719  ideqg  5720  dmopab2rex  5786  elrnmpt  5825  elrnmpt1  5827  elrnmptg  5828  restidsing  5922  somin1  5998  cnveqb  6059  reu3op  6155  reuop  6156  ordequn  6313  funopg  6414  f0rn0  6604  fvelrnb  6773  fvmptg  6816  fndmin  6865  eldmrexrn  6910  foelrn  6925  foco2  6926  fmptco  6944  funopsn  6963  funsndifnop  6966  fmptsng  6983  fmptsnd  6984  tpres  7016  eufnfv  7045  elabrex  7056  abrexco  7057  f1veqaeq  7069  fpropnf1  7079  nf1const  7114  isosolem  7156  f1oiso  7160  eusvobj2  7206  oprabidw  7244  oprabid  7245  f1opr  7267  oprabv  7271  0mpo0  7294  mpofunOLD  7335  elrnmpog  7345  elrnmpo  7346  elrnmpores  7347  ralrnmpo  7348  ov3  7371  ov6g  7372  ovelrn  7384  caovcang  7409  caovcan  7412  uniuni  7547  orduninsuc  7622  funcnvuni  7709  fiunlem  7715  fiun  7716  f1iun  7717  f1oweALT  7745  opiota  7829  eloprabi  7833  frxp  7893  funsssuppss  7932  dftpos4  7987  tz7.44-2  8143  tz7.44-3  8144  oev  8241  oalimcl  8288  omlimcl  8306  odi  8307  omeu  8313  oeeui  8330  nneob  8381  omopth  8387  elqsg  8450  qsdisj  8476  qsel  8478  brecop  8492  eroveu  8494  erovlem  8495  elixpsn  8618  ixpsnf1o  8619  boxcutc  8622  2dom  8707  fundmen  8708  xpf1o  8808  nneneq  8829  fofinf1o  8951  elfi  9029  elfiun  9046  dffi3  9047  brwdom  9183  brwdom3  9198  unwdomg  9200  xpwdomg  9201  noinfep  9275  cantnfp1lem1  9293  cantnfp1lem3  9295  cantnflem1  9304  scott0  9502  updjudhcoinrg  9549  updjud  9550  carden2a  9582  cardiun  9598  pm54.43lem  9616  alephval3  9724  dfac5lem3  9739  dfac5lem4  9740  dfac2b  9744  kmlem9  9772  kmlem12  9775  cardcf  9866  cfeq0  9870  cfsuc  9871  cff1  9872  cflim2  9877  cfss  9879  isfin5  9913  fin1a2lem11  10024  fin1a2lem13  10026  brdom7disj  10145  brdom6disj  10146  canthp1lem2  10267  canthp1  10268  tskuni  10397  gruina  10432  genpv  10613  genpelv  10614  addsrmo  10687  mulsrmo  10688  ltsosr  10708  ltresr  10754  axcnre  10778  axpre-lttri  10779  ltordlem  11357  ltord1  11358  fimaxre3  11778  supaddc  11799  supadd  11800  supmul1  11801  supmullem1  11802  supmullem2  11803  supmul  11804  creur  11824  creui  11825  nn1m1nn  11851  elz  12178  nn0ind-raph  12277  xnegeq  12797  xmullem2  12855  xmulasslem  12875  fleqceilz  13427  fseqsupubi  13551  sqeqor  13784  nn0opth2  13838  hash1snb  13986  hash2prde  14036  prprrab  14039  hash2pwpr  14042  fi1uzind  14063  wrd2ind  14288  cshfn  14355  cshf1  14375  2cshwcshw  14390  scshwfzeqfzo  14391  pfx2  14512  s3iunsndisj  14531  relexpsucnnr  14588  relexprelg  14601  rtrclreclem3  14623  shftfval  14633  sgnval  14651  sqrlem6  14811  reusq0  15026  summo  15281  fsum  15284  telfsumo  15366  infcvgaux1i  15421  infcvgaux2i  15422  mertenslem1  15448  mertenslem2  15449  mertens  15450  prodmo  15498  fprod  15503  ruclem12  15802  mod2eq1n2dvds  15908  divalg  15964  ndvdssub  15970  sadcp1  16014  smupp1  16039  gcdval  16055  bezoutlem1  16099  bezoutlem3  16101  bezoutlem4  16102  bezout  16103  lcmval  16149  coprmgcdb  16206  coprmdvds1  16209  divgcdcoprmex  16223  dvdsprime  16244  nprm  16245  dvdsprm  16260  coprm  16268  qnumval  16293  qdenval  16294  m1dvdsndvds  16351  reumodprminv  16357  pcval  16397  pceu  16399  pczpre  16400  pcdiv  16405  4sqlem2  16502  4sqlem4  16505  4sqlem12  16509  4sq  16517  vdwapval  16526  vdwapun  16527  vdwlem6  16539  cshwrepswhash1  16656  acsfn  17162  initoid  17507  termoid  17508  cat1lem  17602  posi  17824  gsumval2a  18157  smndex2dnrinv  18342  mgm2nsgrplem2  18346  mgm2nsgrplem3  18347  sgrp2nmndlem5  18356  mgmnsgrpex  18358  sgrpnmndex  18359  cyccom  18610  ghmf1  18651  conjnmzb  18657  orbsta  18707  symgextfv  18810  symgextfo  18814  symgfixfo  18831  pmtrprfval  18879  pmtrprfvalrn  18880  psgneu  18898  psgnval  18899  psgnvali  18900  psgnvalii  18901  odfval  18924  odval  18926  dfod2  18955  submod  18958  isslw  18997  sylow2alem1  19006  sylow3lem2  19017  lsmelvalm  19040  lsmdisj2  19072  efgrelexlemb  19140  frgpup3lem  19167  cyggeninv  19267  cygablOLD  19276  gsumval3eu  19289  gsumval3lem2  19291  gsummpt1n0  19350  nn0gsumfz  19369  dprddisj2  19426  dpjrid  19449  pgpfac1lem3  19464  f1rhm0to0ALT  19761  abveq0  19862  abvtrivd  19876  lss1d  20000  lspsn  20039  lspsnel  20040  lspprel  20131  rrgeq0i  20327  domneq0  20335  prmirredlem  20459  znf1o  20516  znfld  20525  znunit  20528  cygznlem3  20534  psgndif  20564  ipeq0  20600  obsip  20683  frlmphl  20743  uvcvval  20748  ellspd  20764  psrlidm  20928  psrridm  20929  mvrval2  20947  mvrf1  20950  mplmonmul  20993  evlslem3  21040  mhpsclcl  21087  coe1tm  21194  coe1tmfv2  21196  cply1coe0  21220  cply1coe0bi  21221  gsummoncoe1  21225  mamufacex  21288  mat1comp  21337  mat1dimelbas  21368  mat1dimid  21371  scmatel  21402  scmateALT  21409  mavmulsolcl  21448  marrepeval  21460  marepveval  21465  mdetunilem8  21516  maducoeval2  21537  madugsum  21540  minmar1eval  21546  symgmatr01lem  21550  symgmatr01  21551  gsummatr01lem3  21554  gsummatr01lem4  21555  gsummatr01  21556  m2cpm  21638  m2cpminvid2lem  21651  decpmatid  21667  monmatcollpw  21676  pmatcollpw3fi1lem1  21683  mp2pm2mplem4  21706  fvmptnn04ifc  21749  chfacffsupp  21753  chfacfscmul0  21755  chfacfscmulgsum  21757  chfacfpmmul0  21759  chfacfpmmulgsum  21761  cpmadumatpoly  21780  cayleyhamilton  21787  cayleyhamiltonALT  21788  istopon  21809  toponsspwpw  21819  fctop  21901  cctop  21903  ppttop  21904  pptbas  21905  epttop  21906  t0sep  22221  t1sep2  22266  cmpsublem  22296  cmpsub  22297  unisngl  22424  txuni2  22462  elpt  22469  ptbasfi  22478  xkoopn  22486  ptpjopn  22509  ptclsg  22512  dfac14lem  22514  ptcnp  22519  ptrescn  22536  tx1stc  22547  qtopeu  22613  kqt0lem  22633  isr0  22634  hauspwpwf1  22884  xmeteq0  23236  imasf1oxmet  23273  comet  23411  stdbdxmet  23413  met2ndci  23420  prdsxmslem2  23427  nrmmetd  23472  tngngp  23552  tngngp3  23554  xrsxmet  23706  iccpnfcnv  23841  iccpnfhmeo  23842  cnheibor  23852  elovolm  24372  ovolgelb  24377  ovolicc1  24413  ovolicc  24420  ioorval  24471  uniioombllem6  24485  dyadmax  24495  dyadmbl  24497  i1fadd  24592  i1fmul  24593  itg1addlem3  24595  i1fmulc  24601  itg2l  24627  itg2leub  24632  limcmpt  24780  limcco  24790  dvcobr  24843  deg1ldg  24990  ig1pval  25070  elply  25089  elply2  25090  coeval  25117  coe1termlem  25152  coe1term  25153  quotval  25185  plydivlem4  25189  plydivex  25190  vieta1  25205  aannenlem2  25222  aalioulem2  25226  abelthlem9  25332  logtayllem  25547  logtayl  25548  isosctrlem2  25702  leibpilem2  25824  rlimcnp2  25849  efrlim  25852  dvdsmulf1o  26076  perfectlem2  26111  lgsfval  26183  lgsval2lem  26188  lgsqrmodndvds  26234  lgsdchrval  26235  gausslemma2dlem0i  26245  2lgslem1b  26273  2lgslem3  26285  2sqlem2  26299  2sqlem8  26307  2sqlem9  26308  2sqlem11  26310  addsq2reu  26321  dchrisum0flblem1  26389  padicval  26498  padicabv  26511  ostth1  26514  axtgcgrid  26554  axtgbtwnid  26557  islmib  26878  inaghl  26936  axpaschlem  27031  axlowdimlem15  27047  axlowdim  27052  upgredg2vtx  27232  edglnl  27234  umgredgnlp  27238  usgredg2vtxeuALT  27310  uspgredg2v  27312  ushgredgedgloop  27319  nbusgredgeu  27454  cusgrfilem2  27544  cusgrfi  27546  vtxdushgrfvedg  27578  1loopgrvd2  27591  rusgr1vtxlem  27675  wlkeq  27721  wlkp1lem8  27768  upgrwlkdvdelem  27823  crctcshwlkn0lem6  27899  wlknwwlksnbij  27972  rusgrnumwwlkl1  28052  clwlkclwwlklem2a1  28075  clwwlknscsh  28145  eleclclwwlkn  28159  hashecclwwlkn1  28160  umgrhashecclwwlk  28161  clwwlknon1sn  28183  frgr3vlem1  28356  3vfriswmgrlem  28360  frgrncvvdeqlem3  28384  wlkl0  28450  frgrreggt1  28476  nvz  28750  nmosetn0  28846  nmoolb  28852  nmoubi  28853  nmlno0lem  28874  nmlno0i  28875  hvsubeq0  29149  hvaddcan  29151  normsub0  29217  norm1exi  29331  pjhval  29478  omlsii  29484  omlsi  29485  pjoml  29517  h1de2ci  29637  spansneleq  29651  h1datomi  29662  h1datom  29663  spansncv  29734  5oalem6  29740  pj11  29795  nmopsetn0  29946  nmfnsetn0  29959  nmoplb  29988  nmopub  29989  nmfnlb  30005  nmfnleub  30006  nmlnop0iALT  30076  nmlnop0  30079  lnopeq  30090  nmopun  30095  nmcexi  30107  branmfn  30186  pjnmopi  30229  pj3i  30289  atss  30427  atom1d  30434  chirred  30476  cdj3lem2  30516  elabreximd  30574  disjxpin  30646  disjunsn  30652  br8d  30669  fmptcof2  30714  psgnfzto1stlem  31086  sgnsval  31147  linds2eq  31289  mxidlmax  31351  lbsdiflsp0  31421  fedgmullem1  31424  fedgmullem2  31425  madjusmdetlem2  31492  madjusmdet  31495  zarclssn  31537  xrge0iifcnv  31597  xrge0iifcv  31598  xrge0iifhom  31601  xrge0tmd  31609  xrge0tmdALT  31610  esumc  31731  sgn3da  32220  sgnmul  32221  sgnnbi  32224  sgnpbi  32225  sgn0bi  32226  plymulx0  32238  signspval  32243  tgoldbachgt  32355  bnj1468  32539  f1resfz0f1d  32785  acycgrcycl  32822  sconnpi1  32914  cvmlift3lem2  32995  satfv0  33033  satfv1  33038  satfbrsuc  33041  satfrnmapom  33045  satfv0fun  33046  satf0op  33052  sat1el2xp  33054  fmlafvel  33060  fmla1  33062  isfmlasuc  33063  fmlaomn0  33065  gonan0  33067  goaln0  33068  gonar  33070  goalr  33072  fmla0disjsuc  33073  fmlasucdisj  33074  satffunlem1lem1  33077  satffunlem2lem1  33079  dmopab3rexdif  33080  satfv0fvfmla0  33088  sategoelfvb  33094  ex-sategoelel  33096  satfv1fvfmla1  33098  2goelgoanfmla1  33099  ex-sategoelelomsuc  33101  ex-sategoelel12  33102  prv1n  33106  eldifsucnn  33410  br8  33442  br6  33443  br4  33444  rdgprc0  33488  dfrdg2  33490  ssttrcl  33514  sltval2  33596  sltintdifex  33601  sltres  33602  nolt02o  33635  madef  33777  dfbigcup2  33938  elsingles  33957  dfiota3  33962  brimageg  33966  brdomaing  33974  brrangeg  33975  dfrdg4  33990  elaltxp  34014  funtransport  34070  fvtransport  34071  brsegle  34147  funray  34179  fvray  34180  funline  34181  fvline  34183  ellines  34191  linethru  34192  rankeq1o  34210  subtr  34240  subtr2  34241  nn0prpw  34249  bj-elabd2ALT  34850  bj-gabss  34860  bj-imafv  35157  topdifinffinlem  35255  topdifinffin  35256  topdifinfeq  35258  finxpreclem2  35298  finxpreclem3  35301  fvineqsnf1  35318  fvineqsneu  35319  fin2so  35501  ptrest  35513  poimirlem25  35539  poimirlem26  35540  poimirlem27  35541  poimirlem28  35542  poimirlem31  35545  poimirlem32  35546  heicant  35549  mblfinlem2  35552  mblfinlem3  35553  mblfinlem4  35554  ismblfin  35555  itg2addnclem  35565  itg2addnclem3  35567  itg2addnc  35568  ftc1anc  35595  unirep  35608  sdclem2  35637  sdclem1  35638  sdc  35639  fdc  35640  isbnd  35675  heibor1lem  35704  heiborlem4  35709  heiborlem6  35711  heiborlem10  35715  ismgmOLD  35745  maxidlmax  35938  prnc  35962  isfldidl  35963  dmnnzd  35970  qsdisjALTV  36465  eqvrelqsel  36466  riotasvd  36707  lshpdisj  36738  lsat0cv  36784  lcvexchlem4  36788  lcvexchlem5  36789  lshpkrlem1  36861  lshpkrlem2  36862  lshpkrlem3  36863  lshpkrcl  36867  islshpkrN  36871  atnle  37068  glbconxN  37129  isline  37490  ispointN  37493  pmapglbx  37520  ispsubcl2N  37698  lhp2atnle  37784  cdleme43fsv1snlem  38171  cdleme40v  38220  cdlemkid5  38686  cdlemkid  38687  dvhb1dimN  38737  dib1dim  38916  dicopelval  38928  dicelval1sta  38938  diclspsn  38945  dihvalcqpre  38986  dihglblem2aN  39044  dihglblem2N  39045  dih1dimatlem  39080  dihpN  39087  dochfl1  39227  lcfl7N  39252  lcf1o  39302  hvmapvalvalN  39512  hdmapval2lem  39582  sticksstones10  39833  sticksstones12a  39835  metakunt3  39849  metakunt4  39850  metakunt6  39852  metakunt7  39853  metakunt8  39854  metakunt10  39856  metakunt11  39857  metakunt12  39858  metakunt20  39866  metakunt21  39867  metakunt22  39868  metakunt24  39870  evlsbagval  39985  fsuppind  39989  sn-negex12  40106  elrfi  40219  nacsfg  40230  mzpcompact2lem  40276  eldioph2b  40288  eldioph3  40291  eldiophss  40299  diophrex  40300  elnn0rabdioph  40328  rencldnfilem  40345  elpell1qr  40372  elpell14qr  40374  elpell1234qr  40376  jm2.27  40533  rmydioph  40539  expdiophlem2  40547  wepwsolem  40570  aomclem6  40587  lnr2i  40644  lpirlnr  40645  hbtlem2  40652  hbtlem4  40654  hbtlem5  40656  rngunsnply  40701  flcidc  40702  clcnvlem  40907  brtrclfv2  41012  frege55lem1c  41201  frege104  41252  clsk1indlem0  41328  clsk1indlem2  41329  clsk1indlem3  41330  clsk1indlem4  41331  clsk1indlem1  41332  pm13.192  41701  equncomVD  42161  csbingVD  42177  csbsngVD  42186  csbfv12gALTVD  42192  relopabVD  42194  refsum2cnlem1  42253  elabrexg  42262  elrnmptf  42391  foelrnf  42397  upbdrech  42517  ssfiunibd  42521  iccshift  42731  iooshift  42735  fsumf1of  42790  limcperiod  42844  climinf2mpt  42930  climinfmpt  42931  cncfshiftioo  43108  itgiccshift  43196  itgperiod  43197  stoweidlem46  43262  fourierdlem29  43352  fourierdlem37  43360  fourierdlem48  43370  fourierdlem51  43373  fourierdlem54  43376  fourierdlem62  43384  fourierdlem79  43401  fourierdlem81  43403  fourierdlem82  43404  fourierdlem92  43414  fourierdlem96  43418  fourierdlem97  43419  fourierdlem98  43420  fourierdlem99  43421  fourierdlem103  43425  fourierdlem104  43426  fourierdlem105  43427  fourierdlem108  43430  fourierdlem110  43432  fourierdlem112  43434  etransclem1  43451  etransclem5  43455  etransclem17  43467  etransclem32  43482  etransclem41  43491  sge0f1o  43595  sge0resplit  43619  sge0fodjrnlem  43629  nnfoctbdjlem  43668  nnfoctbdj  43669  ovnval  43754  ovnlecvr  43771  ovnpnfelsup  43772  ovn0lem  43778  hoidmvval  43790  hoidmvlelem1  43808  ovnhoilem1  43814  ovnhoi  43816  ovnlecvr2  43823  hoidifhspval3  43832  hspmbllem2  43840  hoimbl  43844  ovnsubadd2  43859  ovolval5lem2  43866  ovolval5lem3  43867  ovolval5  43868  ovnovol  43872  fsetsnf  44217  fsetsnfo  44219  fcoresf1  44235  aiotaval  44259  euoreqb  44273  afv0fv0  44313  afvfv0bi  44316  afvelrnb  44327  afvelrnb0  44328  afv20defat  44396  otiunsndisjX  44443  fun2dmnopgexmpl  44448  2ffzoeq  44493  elsetpreimafvb  44509  imasetpreimafvbijlemfo  44530  fargshiftf1  44566  fargshiftfo  44567  ichnreuop  44597  ichreuopeq  44598  elsprel  44600  spr0nelg  44601  sprel  44609  prelspr  44611  sprsymrelf1lem  44616  sprsymrelfolem2  44618  paireqne  44636  prprelb  44641  prprelprb  44642  reupr  44647  reuopreuprim  44651  fmtnoprmfac1lem  44689  fmtnofac2  44694  m1expevenALTV  44772  odd2np1ALTV  44799  opoeALTV  44808  opeoALTV  44809  perfectALTVlem2  44847  isgbe  44876  isgbow  44877  isgbo  44878  sbgoldbalt  44906  sgoldbeven3prm  44908  mogoldbb  44910  nnsum3primesgbe  44917  nnsum3primesle9  44919  nnsum4primesodd  44921  nnsum4primesoddALTV  44922  isomuspgrlem1  44952  uspgrsprf1  44982  uspgrsprfo  44983  0nodd  45037  1odd  45038  2nodd  45039  0even  45162  1neven  45163  2even  45164  2zlidl  45165  2zrngamgm  45170  2zrngagrp  45174  2zrngmmgm  45177  2zrngnmrid  45181  suppmptcfin  45388  lcoval  45426  linc0scn0  45437  linc1  45439  el0ldep  45480  snlindsntor  45485  blenval  45590  nn0sumshdiglemB  45639  itcoval1  45682  mo0  45832  isthincd2lem1  45981