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 BIA×ABIBA×A
4 ancom BIBA×ABA×ABI
5 bj-elid4 BA×ABI1stB=2ndB
6 5 pm5.32i BA×ABIBA×A1stB=2ndB
7 3 4 6 3bitri BIA×ABA×A1stB=2ndB
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 |-