Theorem bj-elid5

Description: Characterization of the elements of _I . (Contributed by BJ, 22-Jun-2019)

	Ref	Expression
Assertion	bj-elid5	$$⊢A\in \mathrm{I}\leftrightarrow \left(A\in \left(\mathrm{V}\times \mathrm{V}\right)\wedge 1^{st}\left(A\right)=2^{nd}\left(A\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		reli	$$⊢\mathrm{Rel}\mathrm{I}$$
2		df-rel	$$⊢\mathrm{Rel}\mathrm{I}\leftrightarrow \mathrm{I}\subseteq \mathrm{V}\times \mathrm{V}$$
3	1 2	mpbi	$$⊢\mathrm{I}\subseteq \mathrm{V}\times \mathrm{V}$$
4	3	sseli	$$⊢A\in \mathrm{I}\to A\in \left(\mathrm{V}\times \mathrm{V}\right)$$
5		bj-elid4	$$⊢A\in \left(\mathrm{V}\times \mathrm{V}\right)\to \left(A\in \mathrm{I}\leftrightarrow 1^{st}\left(A\right)=2^{nd}\left(A\right)\right)$$
6	4 5	biadanii	$$⊢A\in \mathrm{I}\leftrightarrow \left(A\in \left(\mathrm{V}\times \mathrm{V}\right)\wedge 1^{st}\left(A\right)=2^{nd}\left(A\right)\right)$$