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 ⊢BC∈I↾A↔B∈A∧B=C

Proof

Step Hyp Ref Expression
1 df-br ⊢BI↾AC↔BC∈I↾A
2 bj-idreseqb ⊢BI↾AC↔B∈A∧B=C
3 1 2 bitr3i ⊢BC∈I↾A↔B∈A∧B=C