Theorem bj-eldiag2

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

	Ref	Expression
Assertion	bj-eldiag2	Could not format assertion : No typesetting found for |- ( A e. V -> ( <. B , C >. e. ( _Id ` A ) <-> ( B e. A /\ B = C ) ) ) 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 , C >. e. ( _Id ` A ) <-> <. B , C >. e. ( _I i^i ( A X. A ) ) ) ) : No typesetting found for |- ( A e. V -> ( <. B , C >. e. ( _Id ` A ) <-> <. B , C >. e. ( _I i^i ( A X. A ) ) ) ) with typecode |-
3		elin	$$⊢⟨B,C⟩\in \left(\mathrm{I}\cap \left(A\times A\right)\right)\leftrightarrow \left(⟨B,C⟩\in \mathrm{I}\wedge ⟨B,C⟩\in \left(A\times A\right)\right)$$
4		bj-opelidb1	$$⊢⟨B,C⟩\in \mathrm{I}\leftrightarrow \left(B\in \mathrm{V}\wedge B=C\right)$$
5		opelxp	$$⊢⟨B,C⟩\in \left(A\times A\right)\leftrightarrow \left(B\in A\wedge C\in A\right)$$
6	4 5	anbi12i	$$⊢\left(⟨B,C⟩\in \mathrm{I}\wedge ⟨B,C⟩\in \left(A\times A\right)\right)\leftrightarrow \left(\left(B\in \mathrm{V}\wedge B=C\right)\wedge \left(B\in A\wedge C\in A\right)\right)$$
7		simprl	$$⊢\left(\left(B\in \mathrm{V}\wedge B=C\right)\wedge \left(B\in A\wedge C\in A\right)\right)\to B\in A$$
8		simplr	$$⊢\left(\left(B\in \mathrm{V}\wedge B=C\right)\wedge \left(B\in A\wedge C\in A\right)\right)\to B=C$$
9	7 8	jca	$$⊢\left(\left(B\in \mathrm{V}\wedge B=C\right)\wedge \left(B\in A\wedge C\in A\right)\right)\to \left(B\in A\wedge B=C\right)$$
10		elex	$$⊢B\in A\to B\in \mathrm{V}$$
11	10	anim1i	$$⊢\left(B\in A\wedge B=C\right)\to \left(B\in \mathrm{V}\wedge B=C\right)$$
12		eleq1	$$⊢B=C\to \left(B\in A\leftrightarrow C\in A\right)$$
13	12	biimpcd	$$⊢B\in A\to \left(B=C\to C\in A\right)$$
14	13	imdistani	$$⊢\left(B\in A\wedge B=C\right)\to \left(B\in A\wedge C\in A\right)$$
15	11 14	jca	$$⊢\left(B\in A\wedge B=C\right)\to \left(\left(B\in \mathrm{V}\wedge B=C\right)\wedge \left(B\in A\wedge C\in A\right)\right)$$
16	9 15	impbii	$$⊢\left(\left(B\in \mathrm{V}\wedge B=C\right)\wedge \left(B\in A\wedge C\in A\right)\right)\leftrightarrow \left(B\in A\wedge B=C\right)$$
17	3 6 16	3bitri	$$⊢⟨B,C⟩\in \left(\mathrm{I}\cap \left(A\times A\right)\right)\leftrightarrow \left(B\in A\wedge B=C\right)$$
18	2 17	bitrdi	Could not format ( A e. V -> ( <. B , C >. e. ( _Id ` A ) <-> ( B e. A /\ B = C ) ) ) : No typesetting found for |- ( A e. V -> ( <. B , C >. e. ( _Id ` A ) <-> ( B e. A /\ B = C ) ) ) with typecode |-