Theorem idreseqidinxp

Description: Condition for the identity restriction to be equal to the identity intersection with a Cartesian product. (Contributed by Peter Mazsa, 19-Jul-2018)

	Ref	Expression
Assertion	idreseqidinxp	⊢ ( 𝐴 ⊆ 𝐵 → ( I ∩ ( 𝐴 × 𝐵 ) ) = ( I ↾ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		inxpssres	⊢ ( I ∩ ( 𝐴 × 𝐵 ) ) ⊆ ( I ↾ 𝐴 )
2	1	a1i	⊢ ( 𝐴 ⊆ 𝐵 → ( I ∩ ( 𝐴 × 𝐵 ) ) ⊆ ( I ↾ 𝐴 ) )
3		idresssidinxp	⊢ ( 𝐴 ⊆ 𝐵 → ( I ↾ 𝐴 ) ⊆ ( I ∩ ( 𝐴 × 𝐵 ) ) )
4	2 3	eqssd	⊢ ( 𝐴 ⊆ 𝐵 → ( I ∩ ( 𝐴 × 𝐵 ) ) = ( I ↾ 𝐴 ) )