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 Could not format assertion : No typesetting found for |- ( A e. V -> ( <. B , C >. e. ( _Id ` A ) <-> ( B e. A /\ B = C ) ) ) 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 , C >. e. ( _Id ` A ) <-> <. B , C >. e. ( _I i^i ( A X. A ) ) ) ) : No typesetting found for |- ( A e. V -> ( <. B , C >. e. ( _Id ` A ) <-> <. B , C >. e. ( _I i^i ( A X. A ) ) ) ) with typecode |-
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 syl6bb Could not format ( A e. V -> ( <. B , C >. e. ( _Id ` A ) <-> ( B e. A /\ B = C ) ) ) : No typesetting found for |- ( A e. V -> ( <. B , C >. e. ( _Id ` A ) <-> ( B e. A /\ B = C ) ) ) with typecode |-