Theorem eleq1i 1536

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 1533	. 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 955   e. wcel 957

This theorem is referenced by:  eleq12i 1538  eqeltr 1543  intexrab 2729  reucl 2882  pwexb 2905  ordtri3or 2976  sucexb 3045  xpsspw 3254  inelv 3359  fressnfv 3835  tz7.48-3 3955  f1stres 4090  f2ndres 4091  elxp6 4099  2on 4136  qsexg 4291  fiint 4547  r1pw 4673  zorn2lem4 4778  alephprc 4880  addclprlem2 5106  distrlem1pr 5114  distrlem2pr 5115  supsrlem5 5216  axicn 5257  pnfnre 5483  mnfnre 5484  nn0subt 6122  nnesq 6612  cnpfval 7736  fsumcnlem 7972  nvoprne 8291  sspval 8368  pilem3 8656  grothprimlem 8766  avril1 8768  hhph 9032  hhphOLD 9033  nonbool 9586  pjss2 9616  atssmat 10296  cmphmp 10502  fillsb 10529  sfvlim 10557  rdmob 10632  ishgrag 10713  hgrablkcard 10718

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 962  ax-17 970  ax-4 972  ax-5o 974  ax-ext 1459

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 980  df-cleq 1469  df-clel 1472

Copyright terms: Public domain