Theorem eleqtrri 2280

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

Syntax hints:   = wceq 1372   ∈ wcel 2175

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 1469  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-4 1532  ax-17 1548  ax-ial 1556  ax-ext 2186

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

This theorem is referenced by:  3eltr4i  2286  undifexmid  4236  opi1  4275  opi2  4276  ordpwsucexmid  4617  peano1  4641  acexmidlemcase  5938  acexmidlem2  5940  0lt2o  6526  1lt2o  6527  0elixp  6815  ac6sfi  6994  ctssdccl  7212  exmidomni  7243  exmidonfinlem  7300  exmidfodomrlemr  7309  exmidfodomrlemrALT  7310  exmidaclem  7319  pw1ne3  7341  3nelsucpw1  7345  1lt2pi  7452  prarloclemarch2  7531  prarloclemlt  7605  prarloclemcalc  7614  suplocexprlemdisj  7832  suplocexprlemub  7835  pnfxr  8124  mnfxr  8128  0bits  12241  fnpr2ob  13143  dveflem  15169