Theorem eleq1i 2271

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 2268	. 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 1373   e. wcel 2176

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 1470  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-4 1533  ax-17 1549  ax-ial 1557  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-cleq 2198  df-clel 2201

This theorem is referenced by:  eleq12i  2273  eqeltri  2278  intexrabim  4198  abssexg  4227  abnex  4495  snnex  4496  pwexb  4522  sucexb  4546  omex  4642  iprc  4948  dfse2  5056  fressnfv  5773  fnotovb  5990  f1stres  6247  f2ndres  6248  ottposg  6343  dftpos4  6351  frecabex  6486  oacl  6548  diffifi  6993  djuexb  7148  pitonn  7963  axicn  7978  pnfnre  8116  mnfnre  8117  0mnnnnn0  9329  nprmi  12479  issubm  13337  issrg  13760  srgfcl  13768  subrngrng  13997  txdis1cn  14783  xmeterval  14940  expcncf  15114  gausslemma2dlem1a  15568  2lgslem4  15613  bj-sucexg  15895