Theorem eqeq2i 1485

Description: Inference from equality to equivalence of equalities.

Hypothesis

Ref	Expression
eqeq2i.1	|- A = B

Assertion

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

Proof of Theorem eqeq2i

Step	Hyp	Ref	Expression
1		eqeq2i.1	. 2 |- A = B
2		eqeq2 1484	. 2 |- (A = B -> (C = A <-> C = B))
3	1, 2	ax-mp 7	1 |- (C = A <-> C = B)

Syntax hints:   <-> wb 146   = wceq 956

This theorem is referenced by:  eqeq12i 1488  eqtr 1495  rabid2 1770  dfss2 2058  ssequn1 2200  preq12b 2483  preqsn 2486  pwex 2745  opprc3 2797  opeqpr 2803  wefrc 2943  orddif 3075  onuninsuc 3108  funopg 3547  funimaexg 3575  fnressn 3837  fressnfv 3838  fvresex 3857  abrexexlem2 3859  dfrdg2 3933  rdgsucopab 3946  rdgsucopabn 3947  frsucopab 3954  fnoprval 4017  elxp6 4102  eqerlem 4270  qsid 4301  pwfiOLD 4571  rankr1 4674  ac6lem 4754  cardeq0 4832  card1 4833  cf0 4910  addcompr 5123  mulcompr 5125  axrnegex 5283  axrrecex 5284  pnfnemnf 5536  mul0or 5694  muleqaddt 5700  dfnn2 5936  sqr00t 6714  sqr2irrlem4 6727  cjreb 6781  cjne0t 6831  fsumser0f 7001  fsumser1f 7002  binomlem6 7071  reeff1o 7426  subtop 7646  sn0top 7647  ismet 7798  dfms2 7799  msflem 7803  oprcn 7977  fsumcnlem 7989  isgrp 8041  ringi 8142  vci 8167  spwval2 8653  efifolem2 8723  efifolem6 8727  chnle 9408  h1de2ctlem 9478  cmcmlem 9534  cmcm2 9536  cmbr2 9539  osumcor2 9590  pjss2 9625  ho01 9754  nmop0h 9916  pjclem1 10123  jplem1 10195  atabs2 10329  cdj3lem3 10365  cdj3lem3b 10367  cayleylem3 10411  fine 10449  fineOLD 10450  sfvlimOLD 10606  isalg 10653  algi 10660  dedi 10670  cati 10688  hgralem 10770

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 963  ax-17 971  ax-4 973  ax-5o 975  ax-ext 1459

This theorem depends on definitions:  df-bi 147  df-an 225  df-cleq 1469

Copyright terms: Public domain