Theorem eqeq1i 1728

Description: Inference from equality to equivalence of equalities.

Hypothesis

Ref	Expression
eqeq1i.1	|- A = B

Assertion

Ref	Expression
eqeq1i	|- (A = C <-> B = C)

Proof of Theorem eqeq1i

Step	Hyp	Ref	Expression
1		eqeq1i.1	. 2 |- A = B
2		eqeq1 1727	. 2 |- (A = B -> (A = C <-> B = C))
3	1, 2	ax-mp 7	1 |- (A = C <-> B = C)

Syntax hints:   <-> wb 162   = wceq 1136

This theorem is referenced by:  eqeq12iOLD 1735  ssequn2 2609  sseqin2 2638  dfss4 2654  dfss4OLD 2655  disj 2738  undisj1 2749  undisj2 2750  undif 2778  sbsslemOLD 2803  eusn 2918  uniintsn 3075  iin0 3292  opeqsn 3364  dfepfr 3455  dfepfrOLD 3456  epfrc 3457  epfrcOLD 3458  unisuc 3556  reuuni1 3619  reuuni1OLD 3620  reusnOLD 3630  dmopab3 3980  dm0rn0 3986  dmxpOLD 3989  ssdmres 4046  imadisj 4096  args 4104  dffr3 4108  intirr 4123  dminxp 4168  dmsnn0OLD 4174  dfrel3 4192  fncnv 4290  dff1o4 4455  dff1o4OLD 4456  f1ocnvOLD 4463  fvopab3ig 4552  fopab2 4607  fnotoprb 4727  oprabval 4763  oprabvalig 4764  oprssdm 4786  fparlem1 4892  fparlem2 4893  tz7.44-2 4948  tz7.49c 4980  map0 5214  pw2en 5316  ac6sfi 5320  mapunen 5406  zfreg2 5509  sucprcreg 5513  inf3lem2 5529  zfregs2 5564  rankeq0 5616  rankxpsuc 5635  scott0s 5645  cplem1 5646  zorn2lem7 5752  recexsr 6164  map2psrpr 6168  supsrlem2 6174  subaddi 6324  subadd2i 6326  subsub23i 6327  neg11i 6362  negcon1i 6363  renegcli 6372  renegcliOLD 6373  lesubaddiOLD 6568  divmuli 6690  xrsupss 7082  xrinfmss 7083  elznn0 7153  zltp1le 7185  sqeqori 7688  sqr2irrlem1 7769  crulem 7781  negrebi 7840  abs00i 7888  cvgcmpubi 8241  geoseri 8291  eirrlem5 8450  elcls 8775  islp2 8818  qdensere 8822  metn0 8893  lpbl 8952  bcthlem9 9080  gapmlem 9256  nmlno0lem 9588  logeftb 9913  twpar2 9942  oprabvaligg 9948  fbunfip 10074  hvsubeq0i 10354  hvsubaddi 10357  pjoc2i 10696  pjoml3i 10954  cmbr3i 10968  nonbooli 11023  pjss2i 11052  hosubeq0i 11181  dmadjrnb 11259  nmlnop0iALT 11349  nmcopexlem1 11380  nmcfnexlem1 11409  nmopcoadj0i 11465  pj3lem1 11571  stm1ri 11608  jplem2 11633  atoml2i 11747  irredlem1 11754  cdj3lem3 11802  bnj137 12261  bnj1144 12733  bnj98 13013  sspred 13677  dffr4 13684  wfi 13707  frind 13731  wfrlem8 13756  axsltsolem1 13796  axfelem11 13831  repfuntw 14228  defgelem 14335  clfsebsr 14432  trooo 14481  trinv 14482  vecval3b 14518  vecax3 14521  svli2 14549  efilcp 14636  efilcp2 14640  bwt2 14674  homib 14827  elfiun 15051  compcov 15111  compfipin0 15118  comppfsc 15199  isnrm2 15234  euuni2 15345  disjr 15357  oprabvalg 15388  totbndbnd 15626  pi1gp 15777  zfregs2VD 16324  stb2xpl 16501  stb3xpl 16502  stb2str 16503  stb2v1 16504  stb2v2 16505  stb3str 16509  stb3v1 16510  stb3v2 16511  stb3v3 16512  atombase 16752  grpstr 16826  cnaddablNEW 16868

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 1143  ax-17 1155  ax-4 1157  ax-5o 1159  ax-ext 1702

This theorem depends on definitions:  df-bi 163  df-an 241  df-cleq 1714

Copyright terms: Public domain