Description: Equality theorem for intersection of two classes. (Contributed by NM, 14Dec1993) (Proof shortened by SN, 20Sep2023)
Ref  Expression  

Assertion  ineq1   ( A = B > ( A i^i C ) = ( B i^i C ) ) 
Step  Hyp  Ref  Expression 

1  rabeq   ( A = B > { x e. A  x e. C } = { x e. B  x e. C } ) 

2  dfin5   ( A i^i C ) = { x e. A  x e. C } 

3  dfin5   ( B i^i C ) = { x e. B  x e. C } 

4  1 2 3  3eqtr4g   ( A = B > ( A i^i C ) = ( B i^i C ) ) 