Metamath Proof Explorer

Theorem bj-elid7

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

Ref Expression
Assertion bj-elid7 
|- ( <. B , C >. e. ( _I |` A ) <-> ( B e. A /\ B = C ) )

Proof

Step Hyp Ref Expression
1 df-br 
 |-  ( B ( _I |` A ) C <-> <. B , C >. e. ( _I |` A ) )
2 bj-idreseqb 
 |-  ( B ( _I |` A ) C <-> ( B e. A /\ B = C ) )
3 1 2 bitr3i 
 |-  ( <. B , C >. e. ( _I |` A ) <-> ( B e. A /\ B = C ) )