Theorem eleqtrri 2215

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 2143	. 2 |- B = C
4	1, 3	eleqtri 2214	1 |- A e. C

Syntax hints:   = wceq 1331   e. wcel 1480

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-4 1487  ax-17 1506  ax-ial 1514  ax-ext 2121

This theorem depends on definitions:  df-bi 116  df-cleq 2132  df-clel 2135

This theorem is referenced by:  3eltr4i  2221  undifexmid  4117  opi1  4154  opi2  4155  ordpwsucexmid  4485  peano1  4508  acexmidlemcase  5769  acexmidlem2  5771  0lt2o  6338  1lt2o  6339  0elixp  6623  ac6sfi  6792  ctssdccl  6996  exmidomni  7014  infnninf  7022  nnnninf  7023  exmidonfinlem  7049  exmidfodomrlemr  7058  exmidfodomrlemrALT  7059  exmidaclem  7064  1lt2pi  7148  prarloclemarch2  7227  prarloclemlt  7301  prarloclemcalc  7310  suplocexprlemdisj  7528  suplocexprlemub  7531  pnfxr  7818  mnfxr  7822  dveflem  12855