Theorem eleq1i 1534

Description: Inference from equality to equivalence of membership.

Hypothesis

Ref	Expression
eleq1i.1	|- A = B

Assertion

Ref	Expression
eleq1i	|- (A e. C <-> B e. C)

Proof of Theorem eleq1i

Step	Hyp	Ref	Expression
1		eleq1i.1	. 2 |- A = B
2		eleq1 1531	. 2 |- (A = B -> (A e. C <-> B e. C))
3	1, 2	ax-mp 7	1 |- (A e. C <-> B e. C)

Syntax hints:   <-> wb 146   = wceq 954   e. wcel 956

This theorem is referenced by:  eleq12i 1536  eqeltr 1541  intexrab 2727  reucl 2880  pwexb 2903  ordtri3or 2974  sucexb 3043  xpsspw 3252  inelv 3354  fressnfv 3829  tz7.48-3 3949  f1stres 4083  f2ndres 4084  elxp6 4092  2on 4129  qsexg 4284  fiint 4540  r1pw 4666  zorn2lem4 4771  alephprc 4873  addclprlem2 5099  distrlem1pr 5107  distrlem2pr 5108  supsrlem5 5209  axicn 5250  pnfnre 5476  mnfnre 5477  nn0subt 6116  nnesq 6600  cnpfval 7707  fsumcnlem 7939  sspval 8329  pilem3 8611  grothprimlem 8721  avril1 8723  hhph 8984  nonbool 9536  pjss2 9565  atssmat 10242  cmphmp 10444  fillsb 10471  rdmob 10561  ishgrag 10641  hgrablkcard 10646

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 961  ax-17 969  ax-4 971  ax-5o 973  ax-ext 1457

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 979  df-cleq 1467  df-clel 1470

Copyright terms: Public domain