Theorem eleqtr 1546

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 1538	. 2 |- (A e. B <-> A e. C)
4	1, 3	mpbi 189	1 |- A e. C

Syntax hints:   = wceq 956   e. wcel 958

This theorem is referenced by:  eleqtrr 1547  pri2 2451  rankpw 4684  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 8136  sincnlem 8666  hhshsslem2 9138

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 963  ax-17 971  ax-4 973  ax-5o 975  ax-ext 1459

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

Copyright terms: Public domain