Metamath Proof Explorer


Theorem bj-elid4

Description: Characterization of the elements of _I . (Contributed by BJ, 22-Jun-2019)

Ref Expression
Assertion bj-elid4 ( 𝐴 ∈ ( 𝑉 × 𝑊 ) → ( 𝐴 ∈ I ↔ ( 1st𝐴 ) = ( 2nd𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 1st2nd2 ( 𝐴 ∈ ( 𝑉 × 𝑊 ) → 𝐴 = ⟨ ( 1st𝐴 ) , ( 2nd𝐴 ) ⟩ )
2 eleq1 ( 𝐴 = ⟨ ( 1st𝐴 ) , ( 2nd𝐴 ) ⟩ → ( 𝐴 ∈ I ↔ ⟨ ( 1st𝐴 ) , ( 2nd𝐴 ) ⟩ ∈ I ) )
3 2 adantl ( ( 𝐴 ∈ ( 𝑉 × 𝑊 ) ∧ 𝐴 = ⟨ ( 1st𝐴 ) , ( 2nd𝐴 ) ⟩ ) → ( 𝐴 ∈ I ↔ ⟨ ( 1st𝐴 ) , ( 2nd𝐴 ) ⟩ ∈ I ) )
4 fvex ( 2nd𝐴 ) ∈ V
5 4 inex2 ( ( 1st𝐴 ) ∩ ( 2nd𝐴 ) ) ∈ V
6 bj-opelid ( ( ( 1st𝐴 ) ∩ ( 2nd𝐴 ) ) ∈ V → ( ⟨ ( 1st𝐴 ) , ( 2nd𝐴 ) ⟩ ∈ I ↔ ( 1st𝐴 ) = ( 2nd𝐴 ) ) )
7 5 6 mp1i ( ( 𝐴 ∈ ( 𝑉 × 𝑊 ) ∧ 𝐴 = ⟨ ( 1st𝐴 ) , ( 2nd𝐴 ) ⟩ ) → ( ⟨ ( 1st𝐴 ) , ( 2nd𝐴 ) ⟩ ∈ I ↔ ( 1st𝐴 ) = ( 2nd𝐴 ) ) )
8 3 7 bitrd ( ( 𝐴 ∈ ( 𝑉 × 𝑊 ) ∧ 𝐴 = ⟨ ( 1st𝐴 ) , ( 2nd𝐴 ) ⟩ ) → ( 𝐴 ∈ I ↔ ( 1st𝐴 ) = ( 2nd𝐴 ) ) )
9 1 8 mpdan ( 𝐴 ∈ ( 𝑉 × 𝑊 ) → ( 𝐴 ∈ I ↔ ( 1st𝐴 ) = ( 2nd𝐴 ) ) )