Theorem eleq1i 2262

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 2259	. 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 2167

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 1461  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-4 1524  ax-17 1540  ax-ial 1548  ax-ext 2178

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

This theorem is referenced by:  eleq12i  2264  eqeltri  2269  intexrabim  4187  abssexg  4216  abnex  4483  snnex  4484  pwexb  4510  sucexb  4534  omex  4630  iprc  4935  dfse2  5043  fressnfv  5752  fnotovb  5969  f1stres  6221  f2ndres  6222  ottposg  6317  dftpos4  6325  frecabex  6460  oacl  6522  diffifi  6959  djuexb  7114  pitonn  7920  axicn  7935  pnfnre  8073  mnfnre  8074  0mnnnnn0  9286  nprmi  12305  issubm  13151  issrg  13568  srgfcl  13576  subrngrng  13805  txdis1cn  14561  xmeterval  14718  expcncf  14892  gausslemma2dlem1a  15346  2lgslem4  15391  bj-sucexg  15615