Theorem eqeltrri 2213

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 2143	. 2 ⊢ 𝐵 = 𝐴
3		eqeltrr.2	. 2 ⊢ 𝐴 ∈ 𝐶
4	2, 3	eqeltri 2212	1 ⊢ 𝐵 ∈ 𝐶

Syntax hints:   = wceq 1331   ∈ wcel 1480

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 1423  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-4 1487  ax-17 1506  ax-ial 1514  ax-ext 2121

This theorem depends on definitions:  df-bi 116  df-cleq 2132  df-clel 2135

This theorem is referenced by:  3eltr3i  2220  p0ex  4112  epse  4264  unex  4362  ordtri2orexmid  4438  onsucsssucexmid  4442  ordsoexmid  4477  ordtri2or2exmid  4486  nnregexmid  4534  abrexex  6015  opabex3  6020  abrexex2  6022  abexssex  6023  abexex  6024  oprabrexex2  6028  tfr0dm  6219  exmidonfinlem  7049  1lt2pi  7148  prarloclemarch2  7227  prarloclemlt  7301  0cn  7758  resubcli  8025  0reALT  8059  10nn  9197  numsucc  9221  nummac  9226  qreccl  9434  unirnioo  9756  sn0topon  12257  retopbas  12692  blssioo  12714  bj-unex  13117  nninffeq  13216  exmidsbthrlem  13217