Theorem eleq1i 2236

Description: Inference from equality to equivalence of membership. (Contributed by NM, 5-Aug-1993.)

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

Syntax hints:   <-> wb 104   = wceq 1348   e. wcel 2141

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1440  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-4 1503  ax-17 1519  ax-ial 1527  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-cleq 2163  df-clel 2166

This theorem is referenced by:  eleq12i  2238  eqeltri  2243  intexrabim  4137  abssexg  4166  abnex  4430  snnex  4431  pwexb  4457  sucexb  4479  omex  4575  iprc  4877  dfse2  4982  fressnfv  5680  fnotovb  5893  f1stres  6135  f2ndres  6136  ottposg  6231  dftpos4  6239  frecabex  6374  oacl  6436  diffifi  6868  djuexb  7017  pitonn  7797  axicn  7812  pnfnre  7948  mnfnre  7949  0mnnnnn0  9154  nprmi  12065  issubm  12682  txdis1cn  13031  xmeterval  13188  expcncf  13345  bj-sucexg  13917