Theorem inteqi

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

	Ref	Expression
Hypothesis	inteqi.1	⊢ 𝐴 = 𝐵
Assertion	inteqi	⊢ ∩ 𝐴 = ∩ 𝐵

Proof

Step	Hyp	Ref	Expression
1		inteqi.1	⊢ 𝐴 = 𝐵
2		inteq	⊢ ( 𝐴 = 𝐵 → ∩ 𝐴 = ∩ 𝐵 )
3	1 2	ax-mp	⊢ ∩ 𝐴 = ∩ 𝐵