Metamath Proof Explorer


Theorem resundir

Description: Distributive law for restriction over union. (Contributed by NM, 23-Sep-2004)

Ref Expression
Assertion resundir
|- ( ( A u. B ) |` C ) = ( ( A |` C ) u. ( B |` C ) )

Proof

Step Hyp Ref Expression
1 indir
 |-  ( ( A u. B ) i^i ( C X. _V ) ) = ( ( A i^i ( C X. _V ) ) u. ( B i^i ( C X. _V ) ) )
2 df-res
 |-  ( ( A u. B ) |` C ) = ( ( A u. B ) i^i ( C X. _V ) )
3 df-res
 |-  ( A |` C ) = ( A i^i ( C X. _V ) )
4 df-res
 |-  ( B |` C ) = ( B i^i ( C X. _V ) )
5 3 4 uneq12i
 |-  ( ( A |` C ) u. ( B |` C ) ) = ( ( A i^i ( C X. _V ) ) u. ( B i^i ( C X. _V ) ) )
6 1 2 5 3eqtr4i
 |-  ( ( A u. B ) |` C ) = ( ( A |` C ) u. ( B |` C ) )