Metamath Proof Explorer


Theorem inres

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

Ref Expression
Assertion inres ( 𝐴 ∩ ( 𝐵𝐶 ) ) = ( ( 𝐴𝐵 ) ↾ 𝐶 )

Proof

Step Hyp Ref Expression
1 inass ( ( 𝐴𝐵 ) ∩ ( 𝐶 × V ) ) = ( 𝐴 ∩ ( 𝐵 ∩ ( 𝐶 × V ) ) )
2 df-res ( ( 𝐴𝐵 ) ↾ 𝐶 ) = ( ( 𝐴𝐵 ) ∩ ( 𝐶 × V ) )
3 df-res ( 𝐵𝐶 ) = ( 𝐵 ∩ ( 𝐶 × V ) )
4 3 ineq2i ( 𝐴 ∩ ( 𝐵𝐶 ) ) = ( 𝐴 ∩ ( 𝐵 ∩ ( 𝐶 × V ) ) )
5 1 2 4 3eqtr4ri ( 𝐴 ∩ ( 𝐵𝐶 ) ) = ( ( 𝐴𝐵 ) ↾ 𝐶 )