This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem idinxpresid

Description: The intersection of the identity relation with the cartesian square of a class is the restriction of the identity relation to that class. (Contributed by FL, 2-Aug-2009) (Proof shortened by Peter Mazsa, 9-Sep-2022) (Proof shortened by BJ, 23-Dec-2023)

		Ref	Expression
	Assertion	idinxpresid	⊢ ( I ∩ ( 𝐴 × 𝐴 ) ) = ( I ↾ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		idinxpres	⊢ ( I ∩ ( 𝐴 × 𝐴 ) ) = ( I ↾ ( 𝐴 ∩ 𝐴 ) )
2		inidm	⊢ ( 𝐴 ∩ 𝐴 ) = 𝐴
3	2	reseq2i	⊢ ( I ↾ ( 𝐴 ∩ 𝐴 ) ) = ( I ↾ 𝐴 )
4	1 3	eqtri	⊢ ( I ∩ ( 𝐴 × 𝐴 ) ) = ( I ↾ 𝐴 )