Theorem elidinxp

Description: Characterization of the elements of the intersection of the identity relation with a Cartesian product. (Contributed by Peter Mazsa, 9-Sep-2022)

	Ref	Expression
Assertion	elidinxp	⊢ ( 𝐶 ∈ ( I ∩ ( 𝐴 × 𝐵 ) ) ↔ ∃ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) 𝐶 = ⟨ 𝑥 , 𝑥 ⟩ )

Proof

Step	Hyp	Ref	Expression
1		risset	⊢ ( 𝑥 ∈ 𝐵 ↔ ∃ 𝑦 ∈ 𝐵 𝑦 = 𝑥 )
2	1	anbi2ci	⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝐶 = ⟨ 𝑥 , 𝑥 ⟩ ) ↔ ( 𝐶 = ⟨ 𝑥 , 𝑥 ⟩ ∧ ∃ 𝑦 ∈ 𝐵 𝑦 = 𝑥 ) )
3		r19.42v	⊢ ( ∃ 𝑦 ∈ 𝐵 ( 𝐶 = ⟨ 𝑥 , 𝑥 ⟩ ∧ 𝑦 = 𝑥 ) ↔ ( 𝐶 = ⟨ 𝑥 , 𝑥 ⟩ ∧ ∃ 𝑦 ∈ 𝐵 𝑦 = 𝑥 ) )
4		opeq2	⊢ ( 𝑥 = 𝑦 → ⟨ 𝑥 , 𝑥 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ )
5	4	equcoms	⊢ ( 𝑦 = 𝑥 → ⟨ 𝑥 , 𝑥 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ )
6	5	eqeq2d	⊢ ( 𝑦 = 𝑥 → ( 𝐶 = ⟨ 𝑥 , 𝑥 ⟩ ↔ 𝐶 = ⟨ 𝑥 , 𝑦 ⟩ ) )
7	6	pm5.32ri	⊢ ( ( 𝐶 = ⟨ 𝑥 , 𝑥 ⟩ ∧ 𝑦 = 𝑥 ) ↔ ( 𝐶 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑦 = 𝑥 ) )
8		vex	⊢ 𝑦 ∈ V
9	8	ideq	⊢ ( 𝑥 I 𝑦 ↔ 𝑥 = 𝑦 )
10		df-br	⊢ ( 𝑥 I 𝑦 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ I )
11		equcom	⊢ ( 𝑥 = 𝑦 ↔ 𝑦 = 𝑥 )
12	9 10 11	3bitr3i	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ I ↔ 𝑦 = 𝑥 )
13	12	anbi2i	⊢ ( ( 𝐶 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ I ) ↔ ( 𝐶 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑦 = 𝑥 ) )
14	7 13	bitr4i	⊢ ( ( 𝐶 = ⟨ 𝑥 , 𝑥 ⟩ ∧ 𝑦 = 𝑥 ) ↔ ( 𝐶 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ I ) )
15	14	rexbii	⊢ ( ∃ 𝑦 ∈ 𝐵 ( 𝐶 = ⟨ 𝑥 , 𝑥 ⟩ ∧ 𝑦 = 𝑥 ) ↔ ∃ 𝑦 ∈ 𝐵 ( 𝐶 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ I ) )
16	2 3 15	3bitr2i	⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝐶 = ⟨ 𝑥 , 𝑥 ⟩ ) ↔ ∃ 𝑦 ∈ 𝐵 ( 𝐶 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ I ) )
17	16	rexbii	⊢ ( ∃ 𝑥 ∈ 𝐴 ( 𝑥 ∈ 𝐵 ∧ 𝐶 = ⟨ 𝑥 , 𝑥 ⟩ ) ↔ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ( 𝐶 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ I ) )
18		rexin	⊢ ( ∃ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) 𝐶 = ⟨ 𝑥 , 𝑥 ⟩ ↔ ∃ 𝑥 ∈ 𝐴 ( 𝑥 ∈ 𝐵 ∧ 𝐶 = ⟨ 𝑥 , 𝑥 ⟩ ) )
19		elinxp	⊢ ( 𝐶 ∈ ( I ∩ ( 𝐴 × 𝐵 ) ) ↔ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ( 𝐶 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ I ) )
20	17 18 19	3bitr4ri	⊢ ( 𝐶 ∈ ( I ∩ ( 𝐴 × 𝐵 ) ) ↔ ∃ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) 𝐶 = ⟨ 𝑥 , 𝑥 ⟩ )