Theorem eleq1i 2298

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 2295	. 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 105   = wceq 1398   e. wcel 2203

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-17 1575  ax-ial 1583  ax-ext 2214

This theorem depends on definitions:  df-bi 117  df-cleq 2225  df-clel 2228

This theorem is referenced by:  eleq12i  2300  eqeltri  2305  intexrabim  4265  abssexg  4295  abnex  4568  snnex  4569  pwexb  4595  sucexb  4619  omex  4715  iprc  5026  dfse2  5135  fressnfv  5871  fnotovb  6096  f1stres  6353  f2ndres  6354  ottposg  6486  dftpos4  6494  frecabex  6629  oacl  6693  diffifi  7151  djuexb  7335  pitonn  8163  axicn  8178  pnfnre  8315  mnfnre  8316  0mnnnnn0  9528  fcdmnn0fsupp  9549  pfxccatin12lem3  11424  pfxccat3  11426  swrdccat  11427  pfxccat3a  11430  swrdccat3blem  11431  swrdccat3b  11432  nprmi  12821  issubm  13685  issrg  14109  srgfcl  14117  subrngrng  14347  txdis1cn  15143  xmeterval  15300  expcncf  15474  gausslemma2dlem1a  15931  2lgslem4  15976  clwwlknonex2  16434  bj-sucexg  16692