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

Proof

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