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

Metamath Proof Explorer

Theorem elidinxpid

Description: Characterization of the elements of the intersection of the identity relation with a Cartesian square. (Contributed by Peter Mazsa, 9-Sep-2022)

		Ref	Expression
	Assertion	elidinxpid	$⊢ B \in (I \cap (A \times A)) \leftrightarrow \exists x \in A B = ⟨x, x⟩$

Proof

Step	Hyp	Ref	Expression
1		elidinxp	$⊢ B \in (I \cap (A \times A)) \leftrightarrow \exists x \in (A \cap A) B = ⟨x, x⟩$
2		inidm	$⊢ A \cap A = A$
3	2	rexeqi	$⊢ \exists x \in (A \cap A) B = ⟨x, x⟩ \leftrightarrow \exists x \in A B = ⟨x, x⟩$
4	1 3	bitri	$⊢ B \in (I \cap (A \times A)) \leftrightarrow \exists x \in A B = ⟨x, x⟩$