Metamath Proof Explorer


Theorem inres

Description: Move intersection into class restriction. (Contributed by NM, 18-Dec-2008)

Ref Expression
Assertion inres
|- ( A i^i ( B |` C ) ) = ( ( A i^i B ) |` C )

Proof

Step Hyp Ref Expression
1 inass
 |-  ( ( A i^i B ) i^i ( C X. _V ) ) = ( A i^i ( B i^i ( C X. _V ) ) )
2 df-res
 |-  ( ( A i^i B ) |` C ) = ( ( A i^i B ) i^i ( C X. _V ) )
3 df-res
 |-  ( B |` C ) = ( B i^i ( C X. _V ) )
4 3 ineq2i
 |-  ( A i^i ( B |` C ) ) = ( A i^i ( B i^i ( C X. _V ) ) )
5 1 2 4 3eqtr4ri
 |-  ( A i^i ( B |` C ) ) = ( ( A i^i B ) |` C )