Theorem eleqtrri 2281

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

Syntax hints:   = wceq 1373   e. wcel 2176

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 1470  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-4 1533  ax-17 1549  ax-ial 1557  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-cleq 2198  df-clel 2201

This theorem is referenced by:  3eltr4i  2287  undifexmid  4238  opi1  4277  opi2  4278  ordpwsucexmid  4619  peano1  4643  acexmidlemcase  5941  acexmidlem2  5943  0lt2o  6529  1lt2o  6530  0elixp  6818  ac6sfi  6997  ctssdccl  7215  exmidomni  7246  exmidonfinlem  7303  exmidfodomrlemr  7312  exmidfodomrlemrALT  7313  exmidaclem  7322  pw1ne3  7344  3nelsucpw1  7348  1lt2pi  7455  prarloclemarch2  7534  prarloclemlt  7608  prarloclemcalc  7617  suplocexprlemdisj  7835  suplocexprlemub  7838  pnfxr  8127  mnfxr  8131  0bits  12303  fnpr2ob  13205  dveflem  15231