Theorem eqeltrri 2214

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

Syntax hints:   = wceq 1332   ∈ wcel 1481

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 1424  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-4 1488  ax-17 1507  ax-ial 1515  ax-ext 2122

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

This theorem is referenced by:  3eltr3i  2221  p0ex  4120  epse  4272  unex  4370  ordtri2orexmid  4446  onsucsssucexmid  4450  ordsoexmid  4485  ordtri2or2exmid  4494  nnregexmid  4542  abrexex  6023  opabex3  6028  abrexex2  6030  abexssex  6031  abexex  6032  oprabrexex2  6036  tfr0dm  6227  exmidonfinlem  7066  1lt2pi  7172  prarloclemarch2  7251  prarloclemlt  7325  0cn  7782  resubcli  8049  0reALT  8083  10nn  9221  numsucc  9245  nummac  9250  qreccl  9461  unirnioo  9786  sn0topon  12296  retopbas  12731  blssioo  12753  bj-unex  13288  nninffeq  13391  exmidsbthrlem  13392