Theorem eleqtrri 2314

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

Syntax hints:   = wceq 1402   e. wcel 2209

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 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-17 1579  ax-ial 1587  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-cleq 2231  df-clel 2234

This theorem is referenced by:  3eltr4i  2320  undifexmid  4325  opi1  4367  opi2  4368  ordpwsucexmid  4712  peano1  4736  acexmidlemcase  6070  acexmidlem2  6072  0lt2o  6704  1lt2o  6705  0elixp  7001  ac6sfi  7192  ctssdccl  7441  exmidomni  7472  exmidonfinlem  7535  exmidfodomrlemr  7544  exmidfodomrlemrALT  7545  exmidaclem  7554  pw1ne3  7579  3nelsucpw1  7583  1lt2pi  7697  prarloclemarch2  7776  prarloclemlt  7850  prarloclemcalc  7859  suplocexprlemdisj  8077  suplocexprlemub  8080  pnfxr  8368  mnfxr  8372  0bits  12704  fnpr2ob  13638  dveflem  15750  konigsberglem4  16646  3dom  16932