Theorem eqeltrri 2312

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

This proof depends on syntax axioms:   = wceq 1402   ∈ wcel 2209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-17 1579  ax-ial 1587  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-cleq 2231  df-clel 2234

This theorem is used by:  3eltr3i  2319  p0ex  4327  epse  4489  unex  4589  ordtri2orexmid  4672  onsucsssucexmid  4676  ordsoexmid  4711  ordtri2or2exmid  4720  ontri2orexmidim  4721  nnregexmid  4770  abrexex  6350  opabex3  6355  abrexex2  6357  abexssex  6358  abexex  6359  oprabrexex2  6367  tfr0dm  6597  exmidonfinlem  7551  1lt2pi  7713  prarloclemarch2  7792  prarloclemlt  7866  0cn  8324  resubcli  8596  0reALT  8630  10nn  9807  numsucc  9832  nummac  9837  qreccl  10058  unirnioo  10392  fz0to4untppr  10548  cats1fvn  11558  4sqlem19  13217  dec2dvds  13219  mod2xnegi  13227  modsubi  13228  gcdi  13229  ballotfilemth  13339  fn0g  13754  fngzsum  13767  prdsex  14279  sn0topon  15314  retopbas  15749  blssioo  15779  hovercncf  15872  log2ublem2  16222  log2ublog2  16224  ppi1i  16272  cht2  16276  cht3  16277  bpos1lem  16309  lgslem4  16327  konigsberglem1  16934  bj-unex  17150  exmidsbthrlem  17273