Theorem eqeq2 2738

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

Assertion

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

Proof of Theorem eqeq2

Step	Hyp	Ref	Expression
1		id 22	. 2 ⊢ (𝐴 = 𝐵 → 𝐴 = 𝐵)
2	1	eqeq2d 2737	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 2697

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1775  df-cleq 2718

This theorem is referenced by:  eqeq2i  2739  eqeq12OLD  2745  eqtr3  2752  clelab  2872  alexeqg  3635  pm13.183  3652  elab6g  3655  eqeu  3699  moeq3  3705  mo2icl  3707  mob2  3708  euind  3717  reu6i  3721  reu2eqd  3729  reuind  3746  sbc2or  3784  sbc5ALT  3804  csbiebg  3924  eqif  4564  sneq  4633  reusngf  4671  rexreusng  4678  reuprg0  4701  preq1b  4845  preq12bg  4852  preqsn  4860  disji2  5127  disjprgw  5140  disjprg  5141  dtruALT  5384  opth  5474  euotd  5511  solin  5611  ideqg  5850  resieq  5992  cnveqb  6199  cnveq0  6200  reu3op  6295  reuop  6296  iota5  6529  funopg  6585  fneq2  6644  foeq3  6805  tz6.12f  6919  funbrfv  6944  fnbrfvb  6946  fvelimab  6967  elrnrexdm  7095  funsndifnop  7157  fconst5  7215  eufnfv  7238  f1veqaeq  7264  fpropnf1  7274  nf1const  7309  isosolem  7351  f1opr  7473  mpoeq123  7489  ovmpt4g  7565  ov3  7581  ovg  7583  caovcang  7619  caovcan  7622  tfisi  7861  tfindsg  7863  findsg  7902  f1oweALT  7978  seqomlem2  8473  oawordeu  8577  omopth  8684  ereq2  8734  qsdisj  8815  eroveu  8833  2dom  9058  fundmen  9059  xpf1o  9169  nneneq  9236  nneneqOLD  9248  pwfir  9350  cantnflem1  9725  brttrcl  9749  ttrcltr  9752  ttrclss  9756  ttrclselem2  9762  updjud  9970  alephfp  10144  dfac5  10164  cardcf  10286  cfeq0  10290  sornom  10311  fpwwe2cbv  10664  fpwwe2lem3  10667  ltsosr  11128  map2psrpr  11144  axpre-lttri  11199  subval  11492  divval  11916  nn0ind-raph  12708  uzrdgfni  13972  sqeqor  14228  nn0opth2  14284  hashrabsn1  14386  elprchashprn2  14408  hashbclem  14464  hashbc  14465  hash2prde  14484  hash2pwpr  14490  brfi1indALT  14514  wrdind  14725  wrd2ind  14726  reuccatpfxs1lem  14749  cshf1  14813  wrdl3s3  14966  relexpindlem  15063  sqrtval  15237  sqrmo  15251  reusq0  15462  summolem2  15715  prodmolem2  15932  divides  16253  dvdstr  16291  odd2np1lem  16337  ndvdssub  16406  bitsinv1  16437  eucalglt  16581  hashgcdeq  16786  ramcl2lem  17006  ramcl  17026  cshwrepswhash1  17100  imasaddfnlem  17538  fnhomeqhomf  17699  initoeu2lem1  18031  cat1lem  18113  posi  18337  sgrp2nmndlem3  18910  dfgrp2  18952  grpidinv  18988  dfgrp3lem  19028  orbsta  19303  symgfvne  19374  symgfix2  19410  odlem1  19529  gexlem1  19573  slwispgp  19605  sylow3lem6  19626  efgrelexlemb  19744  gsumval3lem2  19900  pgpfac1  20076  pgpfaclem2  20078  pgpfac  20080  ablfaclem1  20081  isdomn  20679  isdomn4  20690  domnlcanb  20694  domnrcanb  20696  obsip  21715  uvcval  21779  mvrval  21987  mhpval  22130  psdfval  22148  coe1tmmul2  22263  coe1tmmul  22264  mat1comp  22430  mat1dimid  22464  scmateALT  22502  marrepval  22552  marepvval  22557  minmar1val  22638  gsummatr01  22649  t0sep  23316  t1sep2  23361  is2ndc  23438  kqt0lem  23728  isr0  23729  isufil2  23900  xmeteq0  24332  imasf1oxmet  24369  xrsxmet  24813  iccpnfcnv  24957  dyadmax  25615  dyadmbl  25617  dvfsumle  26042  dvfsumleOLD  26043  dvfsumabs  26045  dvfsumlem1  26048  mdegle0  26101  fta1g  26194  ig1peu  26199  fta1  26333  aalioulem2  26358  taylthlem2  26399  efopn  26682  efrlim  26994  efrlimOLD  26995  musum  27216  mpodvdsmulf1o  27219  dvdsmulf1o  27221  dchrsum2  27294  sumdchr2  27296  gausslemma2dlem0i  27390  addsqnreup  27469  2sqreulem1  27472  2sqreultblem  27474  2sqreunnlem1  27475  2sqreunnltblem  27477  2sqreulem3  27479  sltres  27689  nosupprefixmo  27727  noinfprefixmo  27728  nosupcbv  27729  nosupno  27730  nosupfv  27733  noinfcbv  27744  noinfno  27745  noinffv  27748  elmade  27888  divsval  28187  noseqrdgfn  28277  axtgcgrid  28387  axtgbtwnid  28390  tglowdim1i  28425  islmib  28711  axcontlem12  28906  upgredgpr  29075  ushgredgedg  29162  ushgredgedgloop  29164  rusgrpropnb  29517  rgrx0ndm  29527  uspgr2wlkeq  29580  wlkson  29590  upgrwlkdvdelem  29670  spthonepeq  29686  iswwlksnon  29784  wlklnwwlkln2lem  29813  wwlksnredwwlkn  29826  wwlksnextprop  29843  wwlksnwwlksnon  29846  elwwlks2ons3  29886  rusgrnumwwlklem  29901  clwlkclwwlklem2a4  29927  clwwlkn  29956  clwwlkext2edg  29986  hashecclwwlkn1  30007  umgrhashecclwwlk  30008  clwwlknon  30020  clwwlk0on0  30022  uhgr3cyclexlem  30111  1conngr  30124  frgr3vlem1  30203  3vfriswmgrlem  30207  frgrwopreglem3  30244  fusgreg2wsplem  30263  fusgreghash2wsp  30268  numclwlk1lem1  30299  numclwwlkovq  30304  numclwwlk2lem1  30306  frgrregord013  30325  friendshipgt3  30328  ex-opab  30362  isgrpoi  30428  grpoidinv2  30445  hvsubeq0  30998  hvaddcan  31000  hvsubadd  31007  normsub0  31066  omlsi  31334  pjoml  31366  nonbooli  31581  pj11  31644  lnopeq  31939  nmopun  31944  pjclem4a  32128  pj3lem1  32136  strlem4  32184  hstrlem4  32192  jplem1  32198  superpos  32284  ifeqeqx  32463  disji2f  32497  disjif2  32501  disjabrex  32502  disjabrexf  32503  disjxpin  32508  disjunsn  32514  ofpreima  32582  fgreu  32589  fcnvgreu  32590  gsumhashmul  32929  domnlcanOLD  33137  ismxidl  33343  xrge0iifcnv  33761  esumpr2  33913  eulerpartlemgvv  34223  eulerpartlemgh  34225  eulerpartlemgs2  34227  sgnsub  34391  plymulx0  34406  lpadmax  34541  lpadright  34543  bnj1321  34885  f1resfz0f1d  34954  subfacp1lem3  35023  pconncn  35065  cnpconn  35071  txpconn  35073  connpconn  35076  cvmlift3lem2  35161  cvmlift3lem4  35163  cvmlift3  35169  snmlflim  35173  iota5f  35559  rankeq1o  36008  nn0prpw  36048  bj-csbsnlem  36622  bj-elgab  36658  bj-restsnss  36803  bj-restsnss2  36804  bj-imdirco  36910  fin2so  37321  poimirlem2  37336  poimirlem18  37352  poimirlem21  37355  poimirlem25  37359  poimirlem26  37360  poimirlem27  37361  mblfinlem2  37372  mbfresfi  37380  cnambfre  37382  ftc1anclem8  37414  fdc  37459  istotbnd  37483  isexid2  37569  isgrpda  37669  ismaxidl  37754  mpobi123f  37876  mptbi12f  37880  disjressuc2  38099  qsdisjALTV  38326  parteq2  38486  lsatcmp  38714  lshpkrlem1  38821  trlval2  39875  cdlemg1cex  40300  cdlemm10N  40830  dicval  40888  lcmineqlem4  41744  grpods  41906  unitscyglem2  41908  unitscyglem3  41909  unitscyglem4  41910  exfinfldd  41912  nnn1suc  42005  resubval  42078  fsuppind  42280  unxpwdom3  42793  dgraalem  42843  dgraaub  42846  onsucf1lem  42972  frege104  43671  pm13.192  44121  2sbc6g  44126  2sbc5g  44127  pm14.122b  44134  equncomVD  44581  csbingVD  44597  csbsngVD  44606  csbxpgVD  44607  csbresgVD  44608  csbrngVD  44609  csbima12gALTVD  44610  csbunigVD  44611  csbfv12gALTVD  44612  relopabVD  44614  dvnprodlem1  45603  dvnprodlem2  45604  dvnprodlem3  45605  dvnprod  45606  fourierdlem42  45806  etransclem11  45902  etransclem12  45903  etransclem33  45924  nnfoctbdjlem  46112  hoimbl  46288  cfsetsnfsetf  46709  aiota0def  46745  euoreqb  46758  funressndmafv2rn  46872  funressnbrafv2  46893  dfatbrafv2b  46894  funbrafv2  46896  fnbrafv2b  46897  elsetpreimafvbi  46999  elsetpreimafveq  47005  imasetpreimafvbijlemfo  47013  fargshiftf1  47049  ichnreuop  47080  paireqne  47119  reupr  47130  isuspgrim0  47487  clnbgrgrim  47517  uspgrsprf1  47560  uspgrsprfo  47561  lidldomn1  47644  nn0sumshdiglem2  48046  mof0  48241  eufsnlem  48244  isthincd2lem1  48384  setrec2lem2  48476