Theorem cleq1i 1108

Description: Inference from equality to equivalence of equalities.

Hypothesis

Ref	Expression
cleq1i.1	|- A = B

Assertion

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

Proof of Theorem cleq1i

Step	Hyp	Ref	Expression
1		cleq1i.1	. 2 |- A = B
2		cleq1 1107	. 2 |- (A = B -> (A = C <-> B = C))
3	1, 2	ax-mp 6	1 |- (A = C <-> B = C)

Syntax hints:   <-> wb 127   = wceq 1091

This theorem is referenced by:  cleq12i 1114  ssequn2 1631  sseqin2 1656  dfss4 1667  rabn0 1716  disj 1733  undisj1 1739  undisj2 1740  ssundif 1764  exss 1881  reuuni1 1955  dfepfr 2184  epfrc 2185  unisuc 2299  dmopab2 2541  dm0rn0 2549  dmxp 2552  ssdmres 2585  dffr3 2620  f1o4 2807  f1ocnv 2811  fvopab3ig 2869  fopab2 2891  tz7.44-2 2967  tz7.49c 2998  oprabval 3047  oprabvalig 3048  elrnoprab 3054  oprssdm 3056  map0 3268  pw2en 3348  mapunen 3397  zfreg2 3448  sucprcreg 3451  inf3lem2 3465  scott0s 3544  cplem1 3545  kmlem3 3582  zornlem6 3608  zornlem7 3609  1pi 3805  recexsr 4010  map2psrpr 4014  supsrlem2 4020  subadd 4143  subsub 4144  subeq0 4163  neg11 4164  negcon1 4165  renegcl 4171  divmul 4218  elznn0 4576  zltp1let 4597  uzwo3lem1 4614  sqe0 4687  sqr2irrlem1 4777  negre 4825  abs00 4839  hvsubeq0 5035  hvsubadd 5038  pjoc2 5273  pjoml3 5496  cmbr3 5509  pjss2 5571  pj3lem1 5658  stm1r 5685  jplem2 5702

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-gen 677  ax-17 925  ax-ext 1074

This theorem depends on definitions:  df-bi 128  df-an 198  df-cleq 1097

metamath.org