Theorem bj-elinxp

Description: Membership in an intersection with a Cartesian product. (Contributed by Peter Mazsa, 9-Sep-2022) Use the x R y idiom and give a shorter proof not depending on df-rel . (Revised by BJ, 16-Oct-2026) Note to remove when moving to main section: a shortening of the exact statement elinxp is possible along the same line.

	Ref	Expression
Assertion	bj-elinxp	⊢ ( 𝐶 ∈ ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) ↔ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ( 𝐶 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑥 𝑅 𝑦 ) )

Proof

Step	Hyp	Ref	Expression
1		elin	⊢ ( 𝐶 ∈ ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) ↔ ( 𝐶 ∈ 𝑅 ∧ 𝐶 ∈ ( 𝐴 × 𝐵 ) ) )
2		elxp2	⊢ ( 𝐶 ∈ ( 𝐴 × 𝐵 ) ↔ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝐶 = ⟨ 𝑥 , 𝑦 ⟩ )
3	2	anbi2i	⊢ ( ( 𝐶 ∈ 𝑅 ∧ 𝐶 ∈ ( 𝐴 × 𝐵 ) ) ↔ ( 𝐶 ∈ 𝑅 ∧ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝐶 = ⟨ 𝑥 , 𝑦 ⟩ ) )
4		r19.42v	⊢ ( ∃ 𝑦 ∈ 𝐵 ( 𝐶 ∈ 𝑅 ∧ 𝐶 = ⟨ 𝑥 , 𝑦 ⟩ ) ↔ ( 𝐶 ∈ 𝑅 ∧ ∃ 𝑦 ∈ 𝐵 𝐶 = ⟨ 𝑥 , 𝑦 ⟩ ) )
5	4	rexbii	⊢ ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ( 𝐶 ∈ 𝑅 ∧ 𝐶 = ⟨ 𝑥 , 𝑦 ⟩ ) ↔ ∃ 𝑥 ∈ 𝐴 ( 𝐶 ∈ 𝑅 ∧ ∃ 𝑦 ∈ 𝐵 𝐶 = ⟨ 𝑥 , 𝑦 ⟩ ) )
6		eleq1	⊢ ( 𝐶 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝐶 ∈ 𝑅 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑅 ) )
7		df-br	⊢ ( 𝑥 𝑅 𝑦 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑅 )
8	6 7	bitr4di	⊢ ( 𝐶 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝐶 ∈ 𝑅 ↔ 𝑥 𝑅 𝑦 ) )
9	8	pm5.32ri	⊢ ( ( 𝐶 ∈ 𝑅 ∧ 𝐶 = ⟨ 𝑥 , 𝑦 ⟩ ) ↔ ( 𝑥 𝑅 𝑦 ∧ 𝐶 = ⟨ 𝑥 , 𝑦 ⟩ ) )
10	9	biancomi	⊢ ( ( 𝐶 ∈ 𝑅 ∧ 𝐶 = ⟨ 𝑥 , 𝑦 ⟩ ) ↔ ( 𝐶 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑥 𝑅 𝑦 ) )
11	10	rexbii	⊢ ( ∃ 𝑦 ∈ 𝐵 ( 𝐶 ∈ 𝑅 ∧ 𝐶 = ⟨ 𝑥 , 𝑦 ⟩ ) ↔ ∃ 𝑦 ∈ 𝐵 ( 𝐶 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑥 𝑅 𝑦 ) )
12	11	rexbii	⊢ ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ( 𝐶 ∈ 𝑅 ∧ 𝐶 = ⟨ 𝑥 , 𝑦 ⟩ ) ↔ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ( 𝐶 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑥 𝑅 𝑦 ) )
13		r19.42v	⊢ ( ∃ 𝑥 ∈ 𝐴 ( 𝐶 ∈ 𝑅 ∧ ∃ 𝑦 ∈ 𝐵 𝐶 = ⟨ 𝑥 , 𝑦 ⟩ ) ↔ ( 𝐶 ∈ 𝑅 ∧ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝐶 = ⟨ 𝑥 , 𝑦 ⟩ ) )
14	5 12 13	3bitr3ri	⊢ ( ( 𝐶 ∈ 𝑅 ∧ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝐶 = ⟨ 𝑥 , 𝑦 ⟩ ) ↔ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ( 𝐶 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑥 𝑅 𝑦 ) )
15	1 3 14	3bitri	⊢ ( 𝐶 ∈ ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) ↔ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ( 𝐶 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑥 𝑅 𝑦 ) )