Metamath Proof Explorer

Theorem ineq1

Description: Equality theorem for intersection of two classes. (Contributed by NM, 14-Dec-1993) (Proof shortened by SN, 20-Sep-2023)

Ref Expression
Assertion ineq1 
|- ( A = B -> ( A i^i C ) = ( B i^i C ) )

Proof

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 ) )