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  4197  abssexg  4226  abnex  4494  snnex  4495  pwexb  4521  sucexb  4545  omex  4641  iprc  4947  dfse2  5055  fressnfv  5771  fnotovb  5988  f1stres  6245  f2ndres  6246  ottposg  6341  dftpos4  6349  frecabex  6484  oacl  6546  diffifi  6991  djuexb  7146  pitonn  7961  axicn  7976  pnfnre  8114  mnfnre  8115  0mnnnnn0  9327  nprmi  12446  issubm  13304  issrg  13727  srgfcl  13735  subrngrng  13964  txdis1cn  14750  xmeterval  14907  expcncf  15081  gausslemma2dlem1a  15535  2lgslem4  15580  bj-sucexg  15858