Theorem eleqtrri 2240

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

Syntax hints:   = wceq 1342   ∈ wcel 2135

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1434  ax-gen 1436  ax-ie1 1480  ax-ie2 1481  ax-4 1497  ax-17 1513  ax-ial 1521  ax-ext 2146

This theorem depends on definitions:  df-bi 116  df-cleq 2157  df-clel 2160

This theorem is referenced by:  3eltr4i  2246  undifexmid  4166  opi1  4204  opi2  4205  ordpwsucexmid  4541  peano1  4565  acexmidlemcase  5831  acexmidlem2  5833  0lt2o  6400  1lt2o  6401  0elixp  6686  ac6sfi  6855  ctssdccl  7067  exmidomni  7097  exmidonfinlem  7140  exmidfodomrlemr  7149  exmidfodomrlemrALT  7150  exmidaclem  7155  pw1ne3  7177  3nelsucpw1  7181  1lt2pi  7272  prarloclemarch2  7351  prarloclemlt  7425  prarloclemcalc  7434  suplocexprlemdisj  7652  suplocexprlemub  7655  pnfxr  7942  mnfxr  7946  dveflem  13228