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 \left(\mathrm{I}\cap \left(A\times A\right)\right)\leftrightarrow \exists x\in AB=⟨x,x⟩$$

Proof

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