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  3956  prex  4112  opkex  4113  idkex  4314  setswithex  4322  0cex  4392  nncex  4396  finex  4397  1cnnc  4408  preaddccan2lem1  4454  ltfinex  4464  ncfinex  4472  tfinex  4485  evenfinex  4503  oddfinex  4504  spfinex  4537  nulnnn  4556  phialllem1  4616  1stex  4739  swapex  4742  ssetex  4744  xpvv  4843  2ndex  5112  fvex  5339  idex  5504  1stfo  5505  2ndfo  5506  swapf1o  5511  ovex  5551  ins4ex  5799  si3ex  5806  cupex  5816  composeex  5820  disjex  5823  addcfnex  5824  funsex  5828  fnsex  5832  crossex  5850  pw1fnex  5852  domfnex  5870  ranfnex  5871  clos1ex  5876  clos1induct  5880  clos1basesuc  5882  transex  5910  refex  5911  antisymex  5912  connexex  5913  foundex  5914  extex  5915  symex  5916  partialex  5917  strictex  5918  weex  5919  erex  5920  enex  6031  enmap2lem1  6063  enmap1lem1  6069  enprmaplem1  6076  enprmaplem4  6079  ncsex  6111  lecex  6115  ltcex  6116  ncex  6117  muccl  6132  mucex  6133  0cnc  6138  nnnc  6146  tcex  6157  tcdi  6164  ceex  6174  ce0addcnnul  6179  ce0nn  6180  ceclb  6183  ce2  6192  sbthlem1  6203  tcfnex  6244  csucex  6259  nncdiv3lem2  6276