Theorem eqeltrri 2162

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

Syntax hints:   = wceq 1290   ∈ wcel 1439

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1382  ax-gen 1384  ax-ie1 1428  ax-ie2 1429  ax-4 1446  ax-17 1465  ax-ial 1473  ax-ext 2071

This theorem depends on definitions:  df-bi 116  df-cleq 2082  df-clel 2085

This theorem is referenced by:  3eltr3i  2169  p0ex  4029  epse  4178  unex  4276  ordtri2orexmid  4352  onsucsssucexmid  4356  ordsoexmid  4391  ordtri2or2exmid  4400  nnregexmid  4447  abrexex  5902  opabex3  5907  abrexex2  5909  abexssex  5910  abexex  5911  oprabrexex2  5915  tfr0dm  6101  1lt2pi  6953  prarloclemarch2  7032  prarloclemlt  7106  0cn  7534  resubcli  7799  0reALT  7833  10nn  8946  numsucc  8970  nummac  8975  qreccl  9181  unirnioo  9445  sn0topon  11842  bj-unex  12076  exmidsbthrlem  12178