Theorem eqeltrri 2261

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

Syntax hints:   = wceq 1363   ∈ wcel 2158

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1457  ax-gen 1459  ax-ie1 1503  ax-ie2 1504  ax-4 1520  ax-17 1536  ax-ial 1544  ax-ext 2169

This theorem depends on definitions:  df-bi 117  df-cleq 2180  df-clel 2183

This theorem is referenced by:  3eltr3i  2268  p0ex  4200  epse  4354  unex  4453  ordtri2orexmid  4534  onsucsssucexmid  4538  ordsoexmid  4573  ordtri2or2exmid  4582  ontri2orexmidim  4583  nnregexmid  4632  abrexex  6131  opabex3  6136  abrexex2  6138  abexssex  6139  abexex  6140  oprabrexex2  6144  tfr0dm  6336  exmidonfinlem  7205  1lt2pi  7352  prarloclemarch2  7431  prarloclemlt  7505  0cn  7962  resubcli  8233  0reALT  8267  10nn  9412  numsucc  9436  nummac  9441  qreccl  9655  unirnioo  9986  fz0to4untppr  10137  prdsex  12735  fn0g  12812  sn0topon  13828  retopbas  14263  blssioo  14285  lgslem4  14644  bj-unex  14911  exmidsbthrlem  15011