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	Could not format assertion : No typesetting found for |- ( A e. V -> ( B e. ( _Id ` A ) <-> ( B e. ( A X. A ) /\ ( 1st ` B ) = ( 2nd ` B ) ) ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		bj-diagval2	Could not format ( A e. V -> ( _Id ` A ) = ( _I i^i ( A X. A ) ) ) : No typesetting found for |- ( A e. V -> ( _Id ` A ) = ( _I i^i ( A X. A ) ) ) with typecode |-
2	1	eleq2d	Could not format ( A e. V -> ( B e. ( _Id ` A ) <-> B e. ( _I i^i ( A X. A ) ) ) ) : No typesetting found for |- ( A e. V -> ( B e. ( _Id ` A ) <-> B e. ( _I i^i ( A X. A ) ) ) ) with typecode |-
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	syl6bb	Could not format ( A e. V -> ( B e. ( _Id ` A ) <-> ( B e. ( A X. A ) /\ ( 1st ` B ) = ( 2nd ` B ) ) ) ) : No typesetting found for |- ( A e. V -> ( B e. ( _Id ` A ) <-> ( B e. ( A X. A ) /\ ( 1st ` B ) = ( 2nd ` B ) ) ) ) with typecode |-