Theorem eleqtri

Description: Substitution of equal classes into membership relation. (Contributed by NM, 15-Jul-1993)

	Ref	Expression
Hypotheses	eleqtri.1	|- A e. B
	eleqtri.2	|- B = C
Assertion	eleqtri	|- A e. C

Proof

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