Theorem eleq1i 2259

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 2256	. 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 1364   e. wcel 2164

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 1458  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-4 1521  ax-17 1537  ax-ial 1545  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-cleq 2186  df-clel 2189

This theorem is referenced by:  eleq12i  2261  eqeltri  2266  intexrabim  4183  abssexg  4212  abnex  4479  snnex  4480  pwexb  4506  sucexb  4530  omex  4626  iprc  4931  dfse2  5039  fressnfv  5746  fnotovb  5962  f1stres  6214  f2ndres  6215  ottposg  6310  dftpos4  6318  frecabex  6453  oacl  6515  diffifi  6952  djuexb  7105  pitonn  7910  axicn  7925  pnfnre  8063  mnfnre  8064  0mnnnnn0  9275  nprmi  12265  issubm  13047  issrg  13464  srgfcl  13472  subrngrng  13701  txdis1cn  14457  xmeterval  14614  expcncf  14788  gausslemma2dlem1a  15215  2lgslem4  15260  bj-sucexg  15484