Theorem eqeq2i 1522

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 1521	. 2 |- (A = B -> (C = A <-> C = B))
3	1, 2	ax-mp 7	1 |- (C = A <-> C = B)

Syntax hints:   <-> wb 144   = wceq 988

This theorem is referenced by:  eqeq12i 1525  eqtri 1532  rabid2 1808  dfss2 2102  ssequn1 2244  preq12b 2531  preqsn 2534  pwex 2797  opprc3 2850  opeqpr 2856  wefrc 2998  orddif 3130  onuninsuci 3163  funopg 3622  funimaexg 3650  fnressn 3913  fressnfv 3914  fvresex 3933  abrexexlem2 3935  dfrdg2 4009  rdgsucopab 4022  rdgsucopabn 4023  frsucopab 4030  fnoprval 4094  elxp6 4178  eqerlem 4354  qsid 4388  rankr1 4760  ac6lem 4840  cardeq0 4919  card1 4920  cf0 4999  addcompr 5212  mulcompr 5214  axrnegex 5372  axrrecex 5373  mul0ori 5780  muleqadd 5786  dfnn2 6023  sqr00 6837  sqr2irrlem4 6850  cjrebi 6904  cjne0 6954  fsumser0fi 7124  fsumser1fi 7125  binomlem6 7194  reeff1o 7550  subtop 7768  sn0top 7769  ismet 7918  dfms2 7919  msflem 7923  oprcn 8097  fsumcnlem 8109  isgrp 8161  ringi 8261  vci 8286  spwval2 8772  efifolem2 8842  efifolem6 8846  chnlei 9528  h1de2ctlem 9598  cmcmlem 9654  cmcm2i 9656  cmbr2i 9659  osumcor2i 9710  pjss2i 9745  ho01i 9874  nmop0h 10033  pjclem1 10241  jplem1 10313  atabs2i 10447  cdj3lem3 10483  cdj3lem3b 10485  cayleylem3 10532  fine 10570  vri 10625  sfvlimOLD 10730  usinuniop 10753  isalg 10788  algi 10795  dedi 10805  cati 10823  hgralem 10912

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 995  ax-17 1003  ax-4 1005  ax-5o 1007  ax-ext 1494

This theorem depends on definitions:  df-bi 145  df-an 223  df-cleq 1505

Copyright terms: Public domain