Metamath Proof Explorer
Description: Equality inference for intersection of two classes. (Contributed by NM, 26Dec1993)


Ref 
Expression 

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

Assertion 
ineq1i 
$${\u22a2}{A}\cap {C}={B}\cap {C}$$ 
Proof
Step 
Hyp 
Ref 
Expression 
1 

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

ineq1 
$${\u22a2}{A}={B}\to {A}\cap {C}={B}\cap {C}$$ 
3 
1 2

axmp 
$${\u22a2}{A}\cap {C}={B}\cap {C}$$ 