Theorem eqeltrri 2281

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

Syntax hints:   = wceq 1373   ∈ wcel 2178

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 1471  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-4 1534  ax-17 1550  ax-ial 1558  ax-ext 2189

This theorem depends on definitions:  df-bi 117  df-cleq 2200  df-clel 2203

This theorem is referenced by:  3eltr3i  2288  p0ex  4248  epse  4407  unex  4506  ordtri2orexmid  4589  onsucsssucexmid  4593  ordsoexmid  4628  ordtri2or2exmid  4637  ontri2orexmidim  4638  nnregexmid  4687  abrexex  6225  opabex3  6230  abrexex2  6232  abexssex  6233  abexex  6234  oprabrexex2  6238  tfr0dm  6431  exmidonfinlem  7332  1lt2pi  7488  prarloclemarch2  7567  prarloclemlt  7641  0cn  8099  resubcli  8370  0reALT  8404  10nn  9554  numsucc  9578  nummac  9583  qreccl  9798  unirnioo  10130  fz0to4untppr  10281  4sqlem19  12847  dec2dvds  12849  modsubi  12857  gcdi  12858  prdsex  13216  fn0g  13322  fngsum  13335  sn0topon  14675  retopbas  15110  blssioo  15140  hovercncf  15233  lgslem4  15595  bj-unex  16054  exmidsbthrlem  16163