Theorem eqeltrri 2239

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

Syntax hints:   = wceq 1343   ∈ wcel 2136

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 1435  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-4 1498  ax-17 1514  ax-ial 1522  ax-ext 2147

This theorem depends on definitions:  df-bi 116  df-cleq 2158  df-clel 2161

This theorem is referenced by:  3eltr3i  2246  p0ex  4166  epse  4319  unex  4418  ordtri2orexmid  4499  onsucsssucexmid  4503  ordsoexmid  4538  ordtri2or2exmid  4547  ontri2orexmidim  4548  nnregexmid  4597  abrexex  6082  opabex3  6087  abrexex2  6089  abexssex  6090  abexex  6091  oprabrexex2  6095  tfr0dm  6286  exmidonfinlem  7145  1lt2pi  7277  prarloclemarch2  7356  prarloclemlt  7430  0cn  7887  resubcli  8157  0reALT  8191  10nn  9333  numsucc  9357  nummac  9362  qreccl  9576  unirnioo  9905  fz0to4untppr  10055  sn0topon  12688  retopbas  13123  blssioo  13145  lgslem4  13504  bj-unex  13761  exmidsbthrlem  13861