Theorem eleqtrri 2216

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

Syntax hints:   = wceq 1332   e. wcel 1481

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 1424  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-4 1488  ax-17 1507  ax-ial 1515  ax-ext 2122

This theorem depends on definitions:  df-bi 116  df-cleq 2133  df-clel 2136

This theorem is referenced by:  3eltr4i  2222  undifexmid  4125  opi1  4162  opi2  4163  ordpwsucexmid  4493  peano1  4516  acexmidlemcase  5777  acexmidlem2  5779  0lt2o  6346  1lt2o  6347  0elixp  6631  ac6sfi  6800  ctssdccl  7004  exmidomni  7022  infnninf  7030  nnnninf  7031  exmidonfinlem  7066  exmidfodomrlemr  7075  exmidfodomrlemrALT  7076  exmidaclem  7081  1lt2pi  7172  prarloclemarch2  7251  prarloclemlt  7325  prarloclemcalc  7334  suplocexprlemdisj  7552  suplocexprlemub  7555  pnfxr  7842  mnfxr  7846  dveflem  12895