Theorem eleqtrri 2283

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

Syntax hints:   = wceq 1373   ∈ wcel 2178

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 1471  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-4 1534  ax-17 1550  ax-ial 1558  ax-ext 2189

This theorem depends on definitions:  df-bi 117  df-cleq 2200  df-clel 2203

This theorem is referenced by:  3eltr4i  2289  undifexmid  4253  opi1  4294  opi2  4295  ordpwsucexmid  4636  peano1  4660  acexmidlemcase  5962  acexmidlem2  5964  0lt2o  6550  1lt2o  6551  0elixp  6839  ac6sfi  7021  ctssdccl  7239  exmidomni  7270  exmidonfinlem  7332  exmidfodomrlemr  7341  exmidfodomrlemrALT  7342  exmidaclem  7351  pw1ne3  7376  3nelsucpw1  7380  1lt2pi  7488  prarloclemarch2  7567  prarloclemlt  7641  prarloclemcalc  7650  suplocexprlemdisj  7868  suplocexprlemub  7871  pnfxr  8160  mnfxr  8164  0bits  12385  fnpr2ob  13287  dveflem  15313