Theorem eleq1i 2180

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 2177	. 2 |- ( A = B -> ( A e. C <-> B e. C ) )
3	1, 2	ax-mp 7	1 |- ( A e. C <-> B e. C )

Syntax hints:   <-> wb 104   = wceq 1314   e. wcel 1463

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1406  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-4 1470  ax-17 1489  ax-ial 1497  ax-ext 2097

This theorem depends on definitions:  df-bi 116  df-cleq 2108  df-clel 2111

This theorem is referenced by:  eleq12i  2182  eqeltri  2187  intexrabim  4038  abssexg  4066  abnex  4328  snnex  4329  pwexb  4355  sucexb  4373  omex  4467  iprc  4765  dfse2  4870  fressnfv  5561  fnotovb  5768  f1stres  6011  f2ndres  6012  ottposg  6106  dftpos4  6114  frecabex  6249  oacl  6310  diffifi  6741  djuexb  6881  pitonn  7583  axicn  7598  pnfnre  7731  mnfnre  7732  0mnnnnn0  8913  nprmi  11651  txdis1cn  12289  xmeterval  12424  expcncf  12578  bj-sucexg  12812