Theorem eleqtrri 2253

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

Syntax hints:   = wceq 1353   e. wcel 2148

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510  ax-17 1526  ax-ial 1534  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-cleq 2170  df-clel 2173

This theorem is referenced by:  3eltr4i  2259  undifexmid  4195  opi1  4234  opi2  4235  ordpwsucexmid  4571  peano1  4595  acexmidlemcase  5872  acexmidlem2  5874  0lt2o  6444  1lt2o  6445  0elixp  6731  ac6sfi  6900  ctssdccl  7112  exmidomni  7142  exmidonfinlem  7194  exmidfodomrlemr  7203  exmidfodomrlemrALT  7204  exmidaclem  7209  pw1ne3  7231  3nelsucpw1  7235  1lt2pi  7341  prarloclemarch2  7420  prarloclemlt  7494  prarloclemcalc  7503  suplocexprlemdisj  7721  suplocexprlemub  7724  pnfxr  8012  mnfxr  8016  fnpr2ob  12764  dveflem  14272