Theorem eleqtr 1549

Description: Substitution of equal classes into membership relation.

Hypotheses

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

Assertion

Ref	Expression
eleqtr	|- A e. C

Proof of Theorem eleqtr

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

Syntax hints:   = wceq 958   e. wcel 960

This theorem is referenced by:  eleqtrr 1550  pri2 2456  rankpw 4701  isum0split 7224  efaddlem3 7347  efaddlem6 7350  efaddlem16 7360  efaddlem18 7362  efaddlem19 7363  eirrlem2 7397  eirrlem3 7398  eirrlem4 7399  eirrlem5 7400  efsep 7403  effsumle 7404  efm1lim 7418  ghgrpilem4 8139  sincnlem 8668  hhshsslem2 9140

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 965  ax-17 973  ax-4 975  ax-5o 977  ax-ext 1462

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 983  df-cleq 1472  df-clel 1475

Copyright terms: Public domain