Metamath Proof Explorer
Description: Equality inference for class intersection. (Contributed by NM, 2Sep2003)


Ref 
Expression 

Hypothesis 
inteqi.1 
$${\u22a2}{A}={B}$$ 

Assertion 
inteqi 
$${\u22a2}\bigcap {A}=\bigcap {B}$$ 
Proof
Step 
Hyp 
Ref 
Expression 
1 

inteqi.1 
$${\u22a2}{A}={B}$$ 
2 

inteq 
$${\u22a2}{A}={B}\to \bigcap {A}=\bigcap {B}$$ 
3 
1 2

axmp 
$${\u22a2}\bigcap {A}=\bigcap {B}$$ 