Theorem inteqi

Description: Equality inference for class intersection. (Contributed by NM, 2-Sep-2003)

	Ref	Expression
Hypothesis	inteqi.1	$$⊢A=B$$
Assertion	inteqi	$$⊢\bigcap A=\bigcap B$$

Proof

Step	Hyp	Ref	Expression
1		inteqi.1	$$⊢A=B$$
2		inteq	$$⊢A=B\to \bigcap A=\bigcap B$$
3	1 2	ax-mp	$$⊢\bigcap A=\bigcap B$$