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	|- ( A e. V -> ( <. B , C >. e. ( _Id ` A ) <-> ( B e. A /\ B = C ) ) )

Proof

Step	Hyp	Ref	Expression
1		bj-diagval2	|- ( A e. V -> ( _Id ` A ) = ( _I i^i ( A X. A ) ) )
2	1	eleq2d	|- ( A e. V -> ( <. B , C >. e. ( _Id ` A ) <-> <. B , C >. e. ( _I i^i ( A X. A ) ) ) )
3		elin	|- ( <. B , C >. e. ( _I i^i ( A X. A ) ) <-> ( <. B , C >. e. _I /\ <. B , C >. e. ( A X. A ) ) )
4		bj-opelidb1	|- ( <. B , C >. e. _I <-> ( B e. _V /\ B = C ) )
5		opelxp	|- ( <. B , C >. e. ( A X. A ) <-> ( B e. A /\ C e. A ) )
6	4 5	anbi12i	|- ( ( <. B , C >. e. _I /\ <. B , C >. e. ( A X. A ) ) <-> ( ( B e. _V /\ B = C ) /\ ( B e. A /\ C e. A ) ) )
7		simprl	|- ( ( ( B e. _V /\ B = C ) /\ ( B e. A /\ C e. A ) ) -> B e. A )
8		simplr	|- ( ( ( B e. _V /\ B = C ) /\ ( B e. A /\ C e. A ) ) -> B = C )
9	7 8	jca	|- ( ( ( B e. _V /\ B = C ) /\ ( B e. A /\ C e. A ) ) -> ( B e. A /\ B = C ) )
10		elex	|- ( B e. A -> B e. _V )
11	10	anim1i	|- ( ( B e. A /\ B = C ) -> ( B e. _V /\ B = C ) )
12		eleq1	|- ( B = C -> ( B e. A <-> C e. A ) )
13	12	biimpcd	|- ( B e. A -> ( B = C -> C e. A ) )
14	13	imdistani	|- ( ( B e. A /\ B = C ) -> ( B e. A /\ C e. A ) )
15	11 14	jca	|- ( ( B e. A /\ B = C ) -> ( ( B e. _V /\ B = C ) /\ ( B e. A /\ C e. A ) ) )
16	9 15	impbii	|- ( ( ( B e. _V /\ B = C ) /\ ( B e. A /\ C e. A ) ) <-> ( B e. A /\ B = C ) )
17	3 6 16	3bitri	|- ( <. B , C >. e. ( _I i^i ( A X. A ) ) <-> ( B e. A /\ B = C ) )
18	2 17	bitrdi	|- ( A e. V -> ( <. B , C >. e. ( _Id ` A ) <-> ( B e. A /\ B = C ) ) )