Theorem eqeltrri 2173

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

Syntax hints:   = wceq 1299   e. wcel 1448

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1391  ax-gen 1393  ax-ie1 1437  ax-ie2 1438  ax-4 1455  ax-17 1474  ax-ial 1482  ax-ext 2082

This theorem depends on definitions:  df-bi 116  df-cleq 2093  df-clel 2096

This theorem is referenced by:  3eltr3i  2180  p0ex  4052  epse  4202  unex  4300  ordtri2orexmid  4376  onsucsssucexmid  4380  ordsoexmid  4415  ordtri2or2exmid  4424  nnregexmid  4472  abrexex  5946  opabex3  5951  abrexex2  5953  abexssex  5954  abexex  5955  oprabrexex2  5959  tfr0dm  6149  1lt2pi  7049  prarloclemarch2  7128  prarloclemlt  7202  0cn  7630  resubcli  7896  0reALT  7930  10nn  9049  numsucc  9073  nummac  9078  qreccl  9284  unirnioo  9597  sn0topon  12039  retopbas  12445  blssioo  12464  bj-unex  12698  nninffeq  12800  exmidsbthrlem  12801