Theorem bj-eldiag

Description: Characterization of the elements of the diagonal of a Cartesian square. Subsumed by bj-elid6 . (Contributed by BJ, 22-Jun-2019)

	Ref	Expression
Assertion	bj-eldiag	$$⊢A\in V\to \left(B\in Id\left(A\right)\leftrightarrow \left(B\in \left(A\times A\right)\wedge 1^{st}\left(B\right)=2^{nd}\left(B\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		bj-diagval2	$$⊢A\in V\to Id\left(A\right)=\mathrm{I}\cap \left(A\times A\right)$$
2	1	eleq2d	$$⊢A\in V\to \left(B\in Id\left(A\right)\leftrightarrow B\in \left(\mathrm{I}\cap \left(A\times A\right)\right)\right)$$
3		elin	$$⊢B\in \left(\mathrm{I}\cap \left(A\times A\right)\right)\leftrightarrow \left(B\in \mathrm{I}\wedge B\in \left(A\times A\right)\right)$$
4		ancom	$$⊢\left(B\in \mathrm{I}\wedge B\in \left(A\times A\right)\right)\leftrightarrow \left(B\in \left(A\times A\right)\wedge B\in \mathrm{I}\right)$$
5		bj-elid4	$$⊢B\in \left(A\times A\right)\to \left(B\in \mathrm{I}\leftrightarrow 1^{st}\left(B\right)=2^{nd}\left(B\right)\right)$$
6	5	pm5.32i	$$⊢\left(B\in \left(A\times A\right)\wedge B\in \mathrm{I}\right)\leftrightarrow \left(B\in \left(A\times A\right)\wedge 1^{st}\left(B\right)=2^{nd}\left(B\right)\right)$$
7	3 4 6	3bitri	$$⊢B\in \left(\mathrm{I}\cap \left(A\times A\right)\right)\leftrightarrow \left(B\in \left(A\times A\right)\wedge 1^{st}\left(B\right)=2^{nd}\left(B\right)\right)$$
8	2 7	bitrdi	$$⊢A\in V\to \left(B\in Id\left(A\right)\leftrightarrow \left(B\in \left(A\times A\right)\wedge 1^{st}\left(B\right)=2^{nd}\left(B\right)\right)\right)$$