Theorem eleqtrri 2242

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

Syntax hints:   = wceq 1343   e. wcel 2136

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 1435  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-4 1498  ax-17 1514  ax-ial 1522  ax-ext 2147

This theorem depends on definitions:  df-bi 116  df-cleq 2158  df-clel 2161

This theorem is referenced by:  3eltr4i  2248  undifexmid  4172  opi1  4210  opi2  4211  ordpwsucexmid  4547  peano1  4571  acexmidlemcase  5837  acexmidlem2  5839  0lt2o  6409  1lt2o  6410  0elixp  6695  ac6sfi  6864  ctssdccl  7076  exmidomni  7106  exmidonfinlem  7149  exmidfodomrlemr  7158  exmidfodomrlemrALT  7159  exmidaclem  7164  pw1ne3  7186  3nelsucpw1  7190  1lt2pi  7281  prarloclemarch2  7360  prarloclemlt  7434  prarloclemcalc  7443  suplocexprlemdisj  7661  suplocexprlemub  7664  pnfxr  7951  mnfxr  7955  dveflem  13327