Theorem eleqtrri 2170

Description: Substitution of equal classes into membership relation. (Contributed by NM, 5-Aug-1993.)

Hypotheses

Ref	Expression
eleqtrr.1	⊢ 𝐴 ∈ 𝐵
eleqtrr.2	⊢ 𝐶 = 𝐵

Assertion

Ref	Expression
eleqtrri	⊢ 𝐴 ∈ 𝐶

Proof of Theorem eleqtrri

Step	Hyp	Ref	Expression
1		eleqtrr.1	. 2 ⊢ 𝐴 ∈ 𝐵
2		eleqtrr.2	. . 3 ⊢ 𝐶 = 𝐵
3	2	eqcomi 2099	. 2 ⊢ 𝐵 = 𝐶
4	1, 3	eleqtri 2169	1 ⊢ 𝐴 ∈ 𝐶

Syntax hints:   = wceq 1296   ∈ wcel 1445

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1388  ax-gen 1390  ax-ie1 1434  ax-ie2 1435  ax-4 1452  ax-17 1471  ax-ial 1479  ax-ext 2077

This theorem depends on definitions:  df-bi 116  df-cleq 2088  df-clel 2091

This theorem is referenced by:  3eltr4i  2176  undifexmid  4049  opi1  4083  opi2  4084  ordpwsucexmid  4414  peano1  4437  acexmidlemcase  5685  acexmidlem2  5687  0lt2o  6243  1lt2o  6244  0elixp  6526  ac6sfi  6694  djuun  6840  exmidomni  6885  infnninf  6893  nnnninf  6894  exmidfodomrlemr  6925  exmidfodomrlemrALT  6926  1lt2pi  6996  prarloclemarch2  7075  prarloclemlt  7149  prarloclemcalc  7158  pnfxr  7637  mnfxr  7641