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

This proof depends on syntax axioms:   = wceq 1402   e. wcel 2209

This proof depends on 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 proof depends on definitions:  df-bi 117  df-cleq 2231  df-clel 2234

This theorem is used by:  eleqtrri  2314  3eltr3i  2319  prid2  3818  2eluzge0  9977  fz01or  10520  fz0to4untppr  10533  ef0lem  12429  ege2le3  12440  efgt1p2  12464  efgt1p  12465  phi1  12999  ballotfilem2  13230  ballotfilem1ri  13280  cnrehmeocntop  15713  dvcjbr  15811  log2ublem2  16090