Theorem eqeltrri 2306

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

Syntax hints:   = wceq 1398   ∈ wcel 2203

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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-17 1575  ax-ial 1583  ax-ext 2214

This theorem depends on definitions:  df-bi 117  df-cleq 2225  df-clel 2228

This theorem is referenced by:  3eltr3i  2313  p0ex  4300  epse  4462  unex  4561  ordtri2orexmid  4644  onsucsssucexmid  4648  ordsoexmid  4683  ordtri2or2exmid  4692  ontri2orexmidim  4693  nnregexmid  4742  abrexex  6309  opabex3  6314  abrexex2  6316  abexssex  6317  abexex  6318  oprabrexex2  6322  tfr0dm  6552  exmidonfinlem  7495  1lt2pi  7651  prarloclemarch2  7730  prarloclemlt  7804  0cn  8262  resubcli  8532  0reALT  8566  10nn  9720  numsucc  9744  nummac  9749  qreccl  9970  unirnioo  10302  fz0to4untppr  10454  cats1fvn  11449  4sqlem19  13100  dec2dvds  13102  modsubi  13110  gcdi  13111  prdsex  13471  fn0g  13577  fngsum  13590  sn0topon  14940  retopbas  15375  blssioo  15405  hovercncf  15498  lgslem4  15863  konigsberglem1  16470  bj-unex  16676  exmidsbthrlem  16789