Theorem eleq1i 2273

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 2270	. 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 2178

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 1471  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-4 1534  ax-17 1550  ax-ial 1558  ax-ext 2189

This theorem depends on definitions:  df-bi 117  df-cleq 2200  df-clel 2203

This theorem is referenced by:  eleq12i  2275  eqeltri  2280  intexrabim  4213  abssexg  4242  abnex  4512  snnex  4513  pwexb  4539  sucexb  4563  omex  4659  iprc  4966  dfse2  5074  fressnfv  5794  fnotovb  6011  f1stres  6268  f2ndres  6269  ottposg  6364  dftpos4  6372  frecabex  6507  oacl  6569  diffifi  7017  djuexb  7172  pitonn  7996  axicn  8011  pnfnre  8149  mnfnre  8150  0mnnnnn0  9362  pfxccatin12lem3  11223  pfxccat3  11225  swrdccat  11226  pfxccat3a  11229  swrdccat3blem  11230  swrdccat3b  11231  nprmi  12561  issubm  13419  issrg  13842  srgfcl  13850  subrngrng  14079  txdis1cn  14865  xmeterval  15022  expcncf  15196  gausslemma2dlem1a  15650  2lgslem4  15695  bj-sucexg  16057