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  6013  acexmidlem2  6015  0lt2o  6609  1lt2o  6610  0elixp  6898  ac6sfi  7087  ctssdccl  7310  exmidomni  7341  exmidonfinlem  7404  exmidfodomrlemr  7413  exmidfodomrlemrALT  7414  exmidaclem  7423  pw1ne3  7448  3nelsucpw1  7452  1lt2pi  7560  prarloclemarch2  7639  prarloclemlt  7713  prarloclemcalc  7722  suplocexprlemdisj  7940  suplocexprlemub  7943  pnfxr  8232  mnfxr  8236  0bits  12538  fnpr2ob  13441  dveflem  15469  konigsberglem4  16361  3dom  16638