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  4177  opi1  4215  opi2  4216  ordpwsucexmid  4552  peano1  4576  acexmidlemcase  5846  acexmidlem2  5848  0lt2o  6418  1lt2o  6419  0elixp  6705  ac6sfi  6874  ctssdccl  7086  exmidomni  7116  exmidonfinlem  7163  exmidfodomrlemr  7172  exmidfodomrlemrALT  7173  exmidaclem  7178  pw1ne3  7200  3nelsucpw1  7204  1lt2pi  7295  prarloclemarch2  7374  prarloclemlt  7448  prarloclemcalc  7457  suplocexprlemdisj  7675  suplocexprlemub  7678  pnfxr  7965  mnfxr  7969  dveflem  13446