Theorem eqeltrri 2240

Description: Substitution of equal classes into membership relation. (Contributed by NM, 5-Aug-1993.)

Hypotheses

Ref	Expression
eqeltrr.1	|- A = B
eqeltrr.2	|- A e. C

Assertion

Ref	Expression
eqeltrri	|- B e. C

Proof of Theorem eqeltrri

Step	Hyp	Ref	Expression
1		eqeltrr.1	. . 3 |- A = B
2	1	eqcomi 2169	. 2 |- B = A
3		eqeltrr.2	. 2 |- A e. C
4	2, 3	eqeltri 2239	1 |- B e. C

Syntax hints:   = wceq 1343   e. wcel 2136

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1435  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-4 1498  ax-17 1514  ax-ial 1522  ax-ext 2147

This theorem depends on definitions:  df-bi 116  df-cleq 2158  df-clel 2161

This theorem is referenced by:  3eltr3i  2247  p0ex  4167  epse  4320  unex  4419  ordtri2orexmid  4500  onsucsssucexmid  4504  ordsoexmid  4539  ordtri2or2exmid  4548  ontri2orexmidim  4549  nnregexmid  4598  abrexex  6085  opabex3  6090  abrexex2  6092  abexssex  6093  abexex  6094  oprabrexex2  6098  tfr0dm  6290  exmidonfinlem  7149  1lt2pi  7281  prarloclemarch2  7360  prarloclemlt  7434  0cn  7891  resubcli  8161  0reALT  8195  10nn  9337  numsucc  9361  nummac  9366  qreccl  9580  unirnioo  9909  fz0to4untppr  10059  fn0g  12606  sn0topon  12728  retopbas  13163  blssioo  13185  lgslem4  13544  bj-unex  13801  exmidsbthrlem  13901