Theorem eqeltrri 2211

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 2141	. 2 ⊢ 𝐵 = 𝐴
3		eqeltrr.2	. 2 ⊢ 𝐴 ∈ 𝐶
4	2, 3	eqeltri 2210	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 2119

This theorem depends on definitions:  df-bi 116  df-cleq 2130  df-clel 2133

This theorem is referenced by:  3eltr3i  2218  p0ex  4107  epse  4259  unex  4357  ordtri2orexmid  4433  onsucsssucexmid  4437  ordsoexmid  4472  ordtri2or2exmid  4481  nnregexmid  4529  abrexex  6008  opabex3  6013  abrexex2  6015  abexssex  6016  abexex  6017  oprabrexex2  6021  tfr0dm  6212  exmidonfinlem  7042  1lt2pi  7141  prarloclemarch2  7220  prarloclemlt  7294  0cn  7751  resubcli  8018  0reALT  8052  10nn  9190  numsucc  9214  nummac  9219  qreccl  9427  unirnioo  9749  sn0topon  12246  retopbas  12681  blssioo  12703  bj-unex  13106  nninffeq  13205  exmidsbthrlem  13206