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

Metamath Proof Explorer

Theorem idinxpres

Description: The intersection of the identity relation with a cartesian product is the restriction of the identity relation to the intersection of the factors. (Contributed by FL, 2-Aug-2009) (Proof shortened by Peter Mazsa, 9-Sep-2022) Generalize statement from cartesian square (now idinxpresid ) to cartesian product. (Revised by BJ, 23-Dec-2023)

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

Proof

Step	Hyp	Ref	Expression
1		elidinxp	⊢ ( 𝑥 ∈ ( I ∩ ( 𝐴 × 𝐵 ) ) ↔ ∃ 𝑦 ∈ ( 𝐴 ∩ 𝐵 ) 𝑥 = ⟨ 𝑦 , 𝑦 ⟩ )
2		elrid	⊢ ( 𝑥 ∈ ( I ↾ ( 𝐴 ∩ 𝐵 ) ) ↔ ∃ 𝑦 ∈ ( 𝐴 ∩ 𝐵 ) 𝑥 = ⟨ 𝑦 , 𝑦 ⟩ )
3	1 2	bitr4i	⊢ ( 𝑥 ∈ ( I ∩ ( 𝐴 × 𝐵 ) ) ↔ 𝑥 ∈ ( I ↾ ( 𝐴 ∩ 𝐵 ) ) )
4	3	eqriv	⊢ ( I ∩ ( 𝐴 × 𝐵 ) ) = ( I ↾ ( 𝐴 ∩ 𝐵 ) )