Theorem eqeltri

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

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

Proof

Step	Hyp	Ref	Expression
1		eqeltri.1	|- A = B
2		eqeltri.2	|- B e. C
3	1	eleq1i	|- ( A e. C <-> B e. C )
4	2 3	mpbir	|- A e. C