Theorem eqeltrri 2251

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

Syntax hints:   = wceq 1353   ∈ wcel 2148

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 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510  ax-17 1526  ax-ial 1534  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-cleq 2170  df-clel 2173

This theorem is referenced by:  3eltr3i  2258  p0ex  4186  epse  4340  unex  4439  ordtri2orexmid  4520  onsucsssucexmid  4524  ordsoexmid  4559  ordtri2or2exmid  4568  ontri2orexmidim  4569  nnregexmid  4618  abrexex  6113  opabex3  6118  abrexex2  6120  abexssex  6121  abexex  6122  oprabrexex2  6126  tfr0dm  6318  exmidonfinlem  7187  1lt2pi  7334  prarloclemarch2  7413  prarloclemlt  7487  0cn  7944  resubcli  8214  0reALT  8248  10nn  9393  numsucc  9417  nummac  9422  qreccl  9636  unirnioo  9967  fz0to4untppr  10117  fn0g  12724  sn0topon  13370  retopbas  13805  blssioo  13827  lgslem4  14186  bj-unex  14442  exmidsbthrlem  14541