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	⊢ ( 𝐴 ∈ 𝑉 → ( ⟨ 𝐵 , 𝐶 ⟩ ∈ ( Id ‘ 𝐴 ) ↔ ( 𝐵 ∈ 𝐴 ∧ 𝐵 = 𝐶 ) ) )

Proof

Step	Hyp	Ref	Expression
1		bj-diagval2	⊢ ( 𝐴 ∈ 𝑉 → ( Id ‘ 𝐴 ) = ( I ∩ ( 𝐴 × 𝐴 ) ) )
2	1	eleq2d	⊢ ( 𝐴 ∈ 𝑉 → ( ⟨ 𝐵 , 𝐶 ⟩ ∈ ( Id ‘ 𝐴 ) ↔ ⟨ 𝐵 , 𝐶 ⟩ ∈ ( I ∩ ( 𝐴 × 𝐴 ) ) ) )
3		elin	⊢ ( ⟨ 𝐵 , 𝐶 ⟩ ∈ ( I ∩ ( 𝐴 × 𝐴 ) ) ↔ ( ⟨ 𝐵 , 𝐶 ⟩ ∈ I ∧ ⟨ 𝐵 , 𝐶 ⟩ ∈ ( 𝐴 × 𝐴 ) ) )
4		bj-opelidb1	⊢ ( ⟨ 𝐵 , 𝐶 ⟩ ∈ I ↔ ( 𝐵 ∈ V ∧ 𝐵 = 𝐶 ) )
5		opelxp	⊢ ( ⟨ 𝐵 , 𝐶 ⟩ ∈ ( 𝐴 × 𝐴 ) ↔ ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ) )
6	4 5	anbi12i	⊢ ( ( ⟨ 𝐵 , 𝐶 ⟩ ∈ I ∧ ⟨ 𝐵 , 𝐶 ⟩ ∈ ( 𝐴 × 𝐴 ) ) ↔ ( ( 𝐵 ∈ V ∧ 𝐵 = 𝐶 ) ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ) ) )
7		simprl	⊢ ( ( ( 𝐵 ∈ V ∧ 𝐵 = 𝐶 ) ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ) ) → 𝐵 ∈ 𝐴 )
8		simplr	⊢ ( ( ( 𝐵 ∈ V ∧ 𝐵 = 𝐶 ) ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ) ) → 𝐵 = 𝐶 )
9	7 8	jca	⊢ ( ( ( 𝐵 ∈ V ∧ 𝐵 = 𝐶 ) ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ) ) → ( 𝐵 ∈ 𝐴 ∧ 𝐵 = 𝐶 ) )
10		elex	⊢ ( 𝐵 ∈ 𝐴 → 𝐵 ∈ V )
11	10	anim1i	⊢ ( ( 𝐵 ∈ 𝐴 ∧ 𝐵 = 𝐶 ) → ( 𝐵 ∈ V ∧ 𝐵 = 𝐶 ) )
12		eleq1	⊢ ( 𝐵 = 𝐶 → ( 𝐵 ∈ 𝐴 ↔ 𝐶 ∈ 𝐴 ) )
13	12	biimpcd	⊢ ( 𝐵 ∈ 𝐴 → ( 𝐵 = 𝐶 → 𝐶 ∈ 𝐴 ) )
14	13	imdistani	⊢ ( ( 𝐵 ∈ 𝐴 ∧ 𝐵 = 𝐶 ) → ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ) )
15	11 14	jca	⊢ ( ( 𝐵 ∈ 𝐴 ∧ 𝐵 = 𝐶 ) → ( ( 𝐵 ∈ V ∧ 𝐵 = 𝐶 ) ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ) ) )
16	9 15	impbii	⊢ ( ( ( 𝐵 ∈ V ∧ 𝐵 = 𝐶 ) ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ) ) ↔ ( 𝐵 ∈ 𝐴 ∧ 𝐵 = 𝐶 ) )
17	3 6 16	3bitri	⊢ ( ⟨ 𝐵 , 𝐶 ⟩ ∈ ( I ∩ ( 𝐴 × 𝐴 ) ) ↔ ( 𝐵 ∈ 𝐴 ∧ 𝐵 = 𝐶 ) )
18	2 17	bitrdi	⊢ ( 𝐴 ∈ 𝑉 → ( ⟨ 𝐵 , 𝐶 ⟩ ∈ ( Id ‘ 𝐴 ) ↔ ( 𝐵 ∈ 𝐴 ∧ 𝐵 = 𝐶 ) ) )