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	⊢ ( ⟨ 𝐵 , 𝐶 ⟩ ∈ ( I ↾ 𝐴 ) ↔ ( 𝐵 ∈ 𝐴 ∧ 𝐵 = 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		df-br	⊢ ( 𝐵 ( I ↾ 𝐴 ) 𝐶 ↔ ⟨ 𝐵 , 𝐶 ⟩ ∈ ( I ↾ 𝐴 ) )
2		bj-idreseqb	⊢ ( 𝐵 ( I ↾ 𝐴 ) 𝐶 ↔ ( 𝐵 ∈ 𝐴 ∧ 𝐵 = 𝐶 ) )
3	1 2	bitr3i	⊢ ( ⟨ 𝐵 , 𝐶 ⟩ ∈ ( I ↾ 𝐴 ) ↔ ( 𝐵 ∈ 𝐴 ∧ 𝐵 = 𝐶 ) )