Theorem xpdisjres

Description: Restriction of a constant function (or other Cartesian product) outside of its domain. (Contributed by Thierry Arnoux, 25-Jan-2017)

	Ref	Expression
Assertion	xpdisjres	|- ( ( A i^i C ) = (/) -> ( ( A X. B ) |` C ) = (/) )

Proof

Step	Hyp	Ref	Expression
1		df-res	|- ( ( A X. B ) |` C ) = ( ( A X. B ) i^i ( C X. _V ) )
2		xpdisj1	|- ( ( A i^i C ) = (/) -> ( ( A X. B ) i^i ( C X. _V ) ) = (/) )
3	1 2	syl5eq	|- ( ( A i^i C ) = (/) -> ( ( A X. B ) |` C ) = (/) )