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 2455  rankpw 4694  isum0split 7217  efaddlem3 7340  efaddlem6 7343  efaddlem16 7353  efaddlem18 7355  efaddlem19 7356  eirrlem2 7390  eirrlem3 7391  eirrlem4 7392  eirrlem5 7393  efsep 7396  effsumle 7397  efm1lim 7411  ghgrpilem4 8132  sincnlem 8661  hhshsslem2 9133

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