Theorem eleqtrri 2246

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

Syntax hints:   = wceq 1348   e. wcel 2141

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 1440  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-4 1503  ax-17 1519  ax-ial 1527  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-cleq 2163  df-clel 2166

This theorem is referenced by:  3eltr4i  2252  undifexmid  4179  opi1  4217  opi2  4218  ordpwsucexmid  4554  peano1  4578  acexmidlemcase  5848  acexmidlem2  5850  0lt2o  6420  1lt2o  6421  0elixp  6707  ac6sfi  6876  ctssdccl  7088  exmidomni  7118  exmidonfinlem  7170  exmidfodomrlemr  7179  exmidfodomrlemrALT  7180  exmidaclem  7185  pw1ne3  7207  3nelsucpw1  7211  1lt2pi  7302  prarloclemarch2  7381  prarloclemlt  7455  prarloclemcalc  7464  suplocexprlemdisj  7682  suplocexprlemub  7685  pnfxr  7972  mnfxr  7976  dveflem  13481