Theorem eqeltri 2423

Description: Substitution of equal classes into membership relation. (Contributed by NM, 5-Aug-1993.)

Hypotheses

Ref	Expression
eqeltr.1	|- A = B
eqeltr.2	|- B e. C

Assertion

Ref	Expression
eqeltri	|- A e. C

Proof of Theorem eqeltri

Step	Hyp	Ref	Expression
1		eqeltr.2	. 2 |- B e. C
2		eqeltr.1	. . 3 |- A = B
3	2	eleq1i 2416	. 2 |- (A e. C <-> B e. C)
4	1, 3	mpbir 200	1 |- A e. C

Syntax hints:   = wceq 1642   e. wcel 1710

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-11 1746  ax-ext 2334

This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1542  df-cleq 2346  df-clel 2349

This theorem is referenced by:  eqeltrri  2424  3eltr4i  2432  intab  3957  prex  4113  opkex  4114  idkex  4315  setswithex  4323  0cex  4393  nncex  4397  finex  4398  1cnnc  4409  preaddccan2lem1  4455  ltfinex  4465  ncfinex  4473  tfinex  4486  evenfinex  4504  oddfinex  4505  spfinex  4538  nulnnn  4557  phialllem1  4617  1stex  4740  swapex  4743  ssetex  4745  xpvv  4844  2ndex  5113  fvex  5340  idex  5505  1stfo  5506  2ndfo  5507  swapf1o  5512  ovex  5552  ins4ex  5800  si3ex  5807  cupex  5817  composeex  5821  disjex  5824  addcfnex  5825  funsex  5829  fnsex  5833  crossex  5851  pw1fnex  5853  domfnex  5871  ranfnex  5872  clos1ex  5877  clos1induct  5881  clos1basesuc  5883  transex  5911  refex  5912  antisymex  5913  connexex  5914  foundex  5915  extex  5916  symex  5917  partialex  5918  strictex  5919  weex  5920  erex  5921  enex  6032  enmap2lem1  6064  enmap1lem1  6070  enprmaplem1  6077  enprmaplem4  6080  ncsex  6112  lecex  6116  ltcex  6117  ncex  6118  muccl  6133  mucex  6134  0cnc  6139  nnnc  6147  tcex  6158  tcdi  6165  ceex  6175  ce0addcnnul  6180  ce0nn  6181  ceclb  6184  ce2  6193  sbthlem1  6204  tcfnex  6245  csucex  6260  nncdiv3lem2  6277