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 )

This proof depends on syntax axioms:   <-> wb 105   = wceq 1402   e. wcel 2209

This proof depends on 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 proof depends on definitions:  df-bi 117  df-cleq 2231  df-clel 2234

This theorem is used by:  eleq12i  2306  eqeltri  2311  intexrabim  4291  abssexg  4321  abnex  4595  snnex  4596  pwexb  4622  sucexb  4646  omex  4742  iprc  5053  dfse2  5163  fressnfv  5905  fnotovb  6134  f1stres  6397  f2ndres  6398  ottposg  6530  dftpos4  6538  frecabex  6673  oacl  6737  diffifi  7202  djuexb  7390  pitonn  8221  axicn  8236  pnfnre  8373  mnfnre  8374  0mnnnnn0  9606  fcdmnn0fsupp  9627  pfxccatin12lem3  11526  pfxccat3  11528  swrdccat  11529  pfxccat3a  11532  swrdccat3blem  11533  swrdccat3b  11534  nprmi  12927  issubm  13838  issrg  14376  srgfcl  14384  subrngrng  14619  txdis1cn  15504  xmeterval  15661  expcncf  15835  ppi2i  16273  gausslemma2dlem1a  16382  2lgslem4  16427  clwwlknonex2  16885  bj-sucexg  17153