Theorem eleqtrri 2310

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

Syntax hints:   = wceq 1398   ∈ wcel 2205

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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-17 1575  ax-ial 1583  ax-ext 2216

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

This theorem is referenced by:  3eltr4i  2316  undifexmid  4308  opi1  4350  opi2  4351  ordpwsucexmid  4694  peano1  4718  acexmidlemcase  6047  acexmidlem2  6049  0lt2o  6676  1lt2o  6677  0elixp  6966  ac6sfi  7157  ctssdccl  7404  exmidomni  7435  exmidonfinlem  7498  exmidfodomrlemr  7507  exmidfodomrlemrALT  7508  exmidaclem  7517  pw1ne3  7542  3nelsucpw1  7546  1lt2pi  7657  prarloclemarch2  7736  prarloclemlt  7810  prarloclemcalc  7819  suplocexprlemdisj  8037  suplocexprlemub  8040  pnfxr  8328  mnfxr  8332  0bits  12649  fnpr2ob  13570  dveflem  15608  konigsberglem4  16503  3dom  16779