bj-elid4

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

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

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

Metamath Proof Explorer