Metamath Proof Explorer


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 I A × A B I B A × A
4 ancom B I B A × A B A × A B I
5 bj-elid4 B A × A B I 1 st B = 2 nd B
6 5 pm5.32i B A × A B I B A × A 1 st B = 2 nd B
7 3 4 6 3bitri B I A × A B A × A 1 st B = 2 nd B
8 2 7 bitrdi 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 |-