Theorem eleq1i 2304

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 2301	. 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 1402   e. wcel 2209

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 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-17 1579  ax-ial 1587  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-cleq 2231  df-clel 2234

This theorem is referenced by:  eleq12i  2306  eqeltri  2311  intexrabim  4284  abssexg  4314  abnex  4588  snnex  4589  pwexb  4615  sucexb  4639  omex  4735  iprc  5046  dfse2  5155  fressnfv  5893  fnotovb  6121  f1stres  6383  f2ndres  6384  ottposg  6516  dftpos4  6524  frecabex  6659  oacl  6723  diffifi  7188  djuexb  7374  pitonn  8205  axicn  8220  pnfnre  8357  mnfnre  8358  0mnnnnn0  9574  fcdmnn0fsupp  9595  pfxccatin12lem3  11482  pfxccat3  11484  swrdccat  11485  pfxccat3a  11488  swrdccat3blem  11489  swrdccat3b  11490  nprmi  12880  issubm  13756  issrg  14243  srgfcl  14251  subrngrng  14483  txdis1cn  15302  xmeterval  15459  expcncf  15633  gausslemma2dlem1a  16091  2lgslem4  16136  clwwlknonex2  16594  bj-sucexg  16862