Theorem eleq1i 2243

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 2240	. 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 1353   e. wcel 2148

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 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510  ax-17 1526  ax-ial 1534  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-cleq 2170  df-clel 2173

This theorem is referenced by:  eleq12i  2245  eqeltri  2250  intexrabim  4151  abssexg  4180  abnex  4445  snnex  4446  pwexb  4472  sucexb  4494  omex  4590  iprc  4892  dfse2  4998  fressnfv  5700  fnotovb  5913  f1stres  6155  f2ndres  6156  ottposg  6251  dftpos4  6259  frecabex  6394  oacl  6456  diffifi  6889  djuexb  7038  pitonn  7842  axicn  7857  pnfnre  7993  mnfnre  7994  0mnnnnn0  9202  nprmi  12114  issubm  12791  issrg  13048  srgfcl  13056  txdis1cn  13560  xmeterval  13717  expcncf  13874  bj-sucexg  14445