Theorem eleqtri 2313

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

Hypotheses

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

Assertion

Ref	Expression
eleqtri	|- A e. C

Proof of Theorem eleqtri

Step	Hyp	Ref	Expression
1		eleqtr.1	. 2 |- A e. B
2		eleqtr.2	. . 3 |- B = C
3	2	eleq2i 2305	. 2 |- ( A e. B <-> A e. C )
4	1, 3	mpbi 145	1 |- A e. C

Syntax hints:   = wceq 1402   e. wcel 2209

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 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-17 1579  ax-ial 1587  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-cleq 2231  df-clel 2234

This theorem is referenced by:  eleqtrri  2314  3eltr3i  2319  prid2  3817  2eluzge0  9958  fz01or  10501  fz0to4untppr  10514  ef0lem  12410  ege2le3  12421  efgt1p2  12445  efgt1p  12446  phi1  12980  ballotfilem2  13211  ballotfilem1ri  13261  cnrehmeocntop  15694  dvcjbr  15792  log2ublem2  16067