Theorem eqeltrri 2111

Description: Substitution of equal classes into membership relation. (Contributed by NM, 5-Aug-1993.)

Hypotheses

Ref	Expression
eqeltrr.1	⊢ 𝐴 = 𝐵
eqeltrr.2	⊢ 𝐴 ∈ 𝐶

Assertion

Ref	Expression
eqeltrri	⊢ 𝐵 ∈ 𝐶

Proof of Theorem eqeltrri

Step	Hyp	Ref	Expression
1		eqeltrr.1	. . 3 ⊢ 𝐴 = 𝐵
2	1	eqcomi 2044	. 2 ⊢ 𝐵 = 𝐴
3		eqeltrr.2	. 2 ⊢ 𝐴 ∈ 𝐶
4	2, 3	eqeltri 2110	1 ⊢ 𝐵 ∈ 𝐶

Syntax hints:   = wceq 1243   ∈ wcel 1393

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1336  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-4 1400  ax-17 1419  ax-ial 1427  ax-ext 2022

This theorem depends on definitions:  df-bi 110  df-cleq 2033  df-clel 2036

This theorem is referenced by:  3eltr3i  2118  p0ex  3939  epse  4079  unex  4176  ordtri2orexmid  4248  onsucsssucexmid  4252  ordsoexmid  4286  ordtri2or2exmid  4296  nnregexmid  4342  abrexex  5744  opabex3  5749  abrexex2  5751  abexssex  5752  abexex  5753  oprabrexex2  5757  tfr0  5937  1lt2pi  6438  prarloclemarch2  6517  prarloclemlt  6591  0cn  7019  resubcli  7274  0reALT  7308  numsucc  8393  nummac  8399  qreccl  8576  unirnioo  8842  bj-unex  10039