Theorem eleq1i 1537

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 1534	. 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 956   e. wcel 958

This theorem is referenced by:  eleq12i 1539  eqeltr 1544  intexrab 2732  reucl 2885  pwexb 2908  ordtri3or 2979  sucexb 3048  xpsspw 3257  inelv 3362  fressnfv 3838  tz7.48-3 3958  f1stres 4093  f2ndres 4094  elxp6 4102  2on 4139  qsexg 4294  fiint 4559  fiintOLD 4560  r1pw 4686  zorn2lem4 4791  alephprc 4893  addclprlem2 5119  distrlem1pr 5127  distrlem2pr 5128  supsrlem5 5229  axicn 5270  pnfnre 5496  mnfnre 5497  nn0subt 6161  nnesq 6662  cnpfval 7757  fsumcnlem 7989  nvoprne 8306  sspval 8382  pilem3 8673  grothprimlem 8782  avril1 8784  hhph 9045  nonbool 9596  pjss2 9625  atssmat 10305  cmphmp 10521  hmeobc 10542  fillsb 10560  sfvlim 10605  sfvlimOLD 10606  rdmob 10681  ishgrag 10769  hgrablkcard 10774

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-ex 981  df-cleq 1469  df-clel 1472

Copyright terms: Public domain