Theorem eqeltrri 2303

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

Syntax hints:   = wceq 1395   ∈ wcel 2200

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 1493  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-4 1556  ax-17 1572  ax-ial 1580  ax-ext 2211

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

This theorem is referenced by:  3eltr3i  2310  p0ex  4276  epse  4437  unex  4536  ordtri2orexmid  4619  onsucsssucexmid  4623  ordsoexmid  4658  ordtri2or2exmid  4667  ontri2orexmidim  4668  nnregexmid  4717  abrexex  6274  opabex3  6279  abrexex2  6281  abexssex  6282  abexex  6283  oprabrexex2  6287  tfr0dm  6483  exmidonfinlem  7397  1lt2pi  7553  prarloclemarch2  7632  prarloclemlt  7706  0cn  8164  resubcli  8435  0reALT  8469  10nn  9619  numsucc  9643  nummac  9648  qreccl  9869  unirnioo  10201  fz0to4untppr  10352  cats1fvn  11338  4sqlem19  12975  dec2dvds  12977  modsubi  12985  gcdi  12986  prdsex  13345  fn0g  13451  fngsum  13464  sn0topon  14805  retopbas  15240  blssioo  15270  hovercncf  15363  lgslem4  15725  bj-unex  16464  exmidsbthrlem  16576