Theorem eleqtrri 2310

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

Syntax hints:   = wceq 1398   e. wcel 2205

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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-17 1575  ax-ial 1583  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-cleq 2227  df-clel 2230

This theorem is referenced by:  3eltr4i  2316  undifexmid  4311  opi1  4353  opi2  4354  ordpwsucexmid  4697  peano1  4721  acexmidlemcase  6053  acexmidlem2  6055  0lt2o  6687  1lt2o  6688  0elixp  6977  ac6sfi  7168  ctssdccl  7415  exmidomni  7446  exmidonfinlem  7509  exmidfodomrlemr  7518  exmidfodomrlemrALT  7519  exmidaclem  7528  pw1ne3  7553  3nelsucpw1  7557  1lt2pi  7671  prarloclemarch2  7750  prarloclemlt  7824  prarloclemcalc  7833  suplocexprlemdisj  8051  suplocexprlemub  8054  pnfxr  8342  mnfxr  8346  0bits  12670  fnpr2ob  13604  dveflem  15717  konigsberglem4  16612  3dom  16888