Metamath Proof Explorer

Theorem bj-eldiag2

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

Ref Expression
Assertion bj-eldiag2 ⊢ A ∈ V → B C ∈ Id ⁡ A ↔ B ∈ A ∧ B = C

Proof

Step Hyp Ref Expression
1 bj-diagval2 ⊢ A ∈ V → Id ⁡ A = I ∩ A × A
2 1 eleq2d ⊢ A ∈ V → B C ∈ Id ⁡ A ↔ B C ∈ I ∩ A × A
3 elin ⊢ B C ∈ I ∩ A × A ↔ B C ∈ I ∧ B C ∈ A × A
4 bj-opelidb1 ⊢ B C ∈ I ↔ B ∈ V ∧ B = C
5 opelxp ⊢ B C ∈ A × A ↔ B ∈ A ∧ C ∈ A
6 4 5 anbi12i ⊢ B C ∈ I ∧ B C ∈ A × A ↔ B ∈ V ∧ B = C ∧ B ∈ A ∧ C ∈ A
7 simprl ⊢ B ∈ V ∧ B = C ∧ B ∈ A ∧ C ∈ A → B ∈ A
8 simplr ⊢ B ∈ V ∧ B = C ∧ B ∈ A ∧ C ∈ A → B = C
9 7 8 jca ⊢ B ∈ V ∧ B = C ∧ B ∈ A ∧ C ∈ A → B ∈ A ∧ B = C
10 elex ⊢ B ∈ A → B ∈ V
11 10 anim1i ⊢ B ∈ A ∧ B = C → B ∈ V ∧ B = C
12 eleq1 ⊢ B = C → B ∈ A ↔ C ∈ A
13 12 biimpcd ⊢ B ∈ A → B = C → C ∈ A
14 13 imdistani ⊢ B ∈ A ∧ B = C → B ∈ A ∧ C ∈ A
15 11 14 jca ⊢ B ∈ A ∧ B = C → B ∈ V ∧ B = C ∧ B ∈ A ∧ C ∈ A
16 9 15 impbii ⊢ B ∈ V ∧ B = C ∧ B ∈ A ∧ C ∈ A ↔ B ∈ A ∧ B = C
17 3 6 16 3bitri ⊢ B C ∈ I ∩ A × A ↔ B ∈ A ∧ B = C
18 2 17 bitrdi ⊢ A ∈ V → B C ∈ Id ⁡ A ↔ B ∈ A ∧ B = C