Theorem eleqtrri 2307

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 2235	. 2 ⊢ 𝐵 = 𝐶
4	1, 3	eleqtri 2306	1 ⊢ 𝐴 ∈ 𝐶

Syntax hints:   = wceq 1397   ∈ wcel 2202

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 1495  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-4 1558  ax-17 1574  ax-ial 1582  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-cleq 2224  df-clel 2227

This theorem is referenced by:  3eltr4i  2313  undifexmid  4283  opi1  4324  opi2  4325  ordpwsucexmid  4668  peano1  4692  acexmidlemcase  6012  acexmidlem2  6014  0lt2o  6608  1lt2o  6609  0elixp  6897  ac6sfi  7086  ctssdccl  7309  exmidomni  7340  exmidonfinlem  7403  exmidfodomrlemr  7412  exmidfodomrlemrALT  7413  exmidaclem  7422  pw1ne3  7447  3nelsucpw1  7451  1lt2pi  7559  prarloclemarch2  7638  prarloclemlt  7712  prarloclemcalc  7721  suplocexprlemdisj  7939  suplocexprlemub  7942  pnfxr  8231  mnfxr  8235  0bits  12519  fnpr2ob  13422  dveflem  15449  3dom  16587