Theorem eqeltrri 2153

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 2086	. 2 |- B = A
3		eqeltrr.2	. 2 |- A e. C
4	2, 3	eqeltri 2152	1 |- B e. C

Syntax hints:   = wceq 1285   e. wcel 1434

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1377  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-4 1441  ax-17 1460  ax-ial 1468  ax-ext 2064

This theorem depends on definitions:  df-bi 115  df-cleq 2075  df-clel 2078

This theorem is referenced by:  3eltr3i  2160  p0ex  3967  epse  4105  unex  4202  ordtri2orexmid  4274  onsucsssucexmid  4278  ordsoexmid  4313  ordtri2or2exmid  4322  nnregexmid  4368  abrexex  5775  opabex3  5780  abrexex2  5782  abexssex  5783  abexex  5784  oprabrexex2  5788  tfr0dm  5971  1lt2pi  6592  prarloclemarch2  6671  prarloclemlt  6745  0cn  7173  resubcli  7438  0reALT  7472  10nn  8573  numsucc  8597  nummac  8602  qreccl  8808  unirnioo  9072  bj-unex  10868