Theorem eleqtrri 2160

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

Syntax hints:   = wceq 1287   e. wcel 1436

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1379  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-4 1443  ax-17 1462  ax-ial 1470  ax-ext 2067

This theorem depends on definitions:  df-bi 115  df-cleq 2078  df-clel 2081

This theorem is referenced by:  3eltr4i  2166  undifexmid  3995  opi1  4026  opi2  4027  ordpwsucexmid  4352  peano1  4375  acexmidlemcase  5589  acexmidlem2  5591  ac6sfi  6547  djuun  6681  exmidomni  6719  fodjuomnilemf  6721  infnninf  6726  nnnninf  6727  exmidfodomrlemr  6749  exmidfodomrlemrALT  6750  1lt2pi  6820  prarloclemarch2  6899  prarloclemlt  6973  prarloclemcalc  6982  pnfxr  7461  mnfxr  7465  0lt2o  11242  1lt2o  11243