Theorem eleqtrri 2163

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

Hypotheses

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

Assertion

Ref	Expression
eleqtrri	|- A e. C

Proof of Theorem eleqtrri

Step	Hyp	Ref	Expression
1		eleqtrr.1	. 2 |- A e. B
2		eleqtrr.2	. . 3 |- C = B
3	2	eqcomi 2092	. 2 |- B = C
4	1, 3	eleqtri 2162	1 |- A e. C

Syntax hints:   = wceq 1289   e. wcel 1438

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1381  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-4 1445  ax-17 1464  ax-ial 1472  ax-ext 2070

This theorem depends on definitions:  df-bi 115  df-cleq 2081  df-clel 2084

This theorem is referenced by:  3eltr4i  2169  undifexmid  4019  opi1  4050  opi2  4051  ordpwsucexmid  4376  peano1  4399  acexmidlemcase  5629  acexmidlem2  5631  ac6sfi  6594  djuun  6739  exmidomni  6777  fodjuomnilemf  6779  infnninf  6784  nnnninf  6785  exmidfodomrlemr  6807  exmidfodomrlemrALT  6808  1lt2pi  6878  prarloclemarch2  6957  prarloclemlt  7031  prarloclemcalc  7040  pnfxr  7519  mnfxr  7523  0lt2o  11531  1lt2o  11532