Theorem eleqtri 1969

Description: Substitution of equal classes into membership relation.

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

Syntax hints:   = wceq 1298   e. wcel 1300

This theorem is referenced by:  eleqtrri 1970  prid2 3107  rankpw 5795  isum0spliti 8478  efaddlem3 8602  efaddlem6 8605  efaddlem16 8615  efaddlem18 8617  efaddlem19 8618  eirrlem2 8652  eirrlem3 8653  eirrlem4 8654  eirrlem5 8655  efsepi 8661  effsumlei 8662  efm1limi 8676  ghgrpilem4 9444  sincnlem 10015  hhshsslem2 10771  cncfres 15895  cnopropabcoc 15918  cnoprab1c 15923  cnoprab2c 15924  phtpycom 16050  phtpycolem3 16053  phtpycolem4 16054  reparphtlem2 16064  pcocn 16076  stb2strx 16747  stb3strx 16754  isgrpiNEW 17115

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 1305  ax-17 1317  ax-4 1319  ax-5o 1321  ax-ext 1865

This theorem depends on definitions:  df-bi 164  df-an 242  df-ex 1327  df-cleq 1877  df-clel 1880

Copyright terms: Public domain