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  9992  fz01or  10536  fz0to4untppr  10549  ef0lem  12453  ege2le3  12464  efgt1p2  12488  efgt1p  12489  phi1  13027  ballotfilem2  13287  ballotfilem1ri  13337  cnrehmeocntop  15848  dvcjbr  15946  log2ublem2  16234