Metamath Proof Explorer

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 ⊢ C ∈ R ∩ A × B ↔ ∃ x ∈ A ∃ y ∈ B C = x y ∧ x R y

Proof

Step Hyp Ref Expression
1 elin ⊢ C ∈ R ∩ A × B ↔ C ∈ R ∧ C ∈ A × B
2 elxp2 ⊢ C ∈ A × B ↔ ∃ x ∈ A ∃ y ∈ B C = x y
3 2 anbi2i ⊢ C ∈ R ∧ C ∈ A × B ↔ C ∈ R ∧ ∃ x ∈ A ∃ y ∈ B C = x y
4 r19.42v ⊢ ∃ y ∈ B C ∈ R ∧ C = x y ↔ C ∈ R ∧ ∃ y ∈ B C = x y
5 4 rexbii ⊢ ∃ x ∈ A ∃ y ∈ B C ∈ R ∧ C = x y ↔ ∃ x ∈ A C ∈ R ∧ ∃ y ∈ B C = x y
6 eleq1 ⊢ C = x y → C ∈ R ↔ x y ∈ R
7 df-br ⊢ x R y ↔ x y ∈ R
8 6 7 bitr4di ⊢ C = x y → C ∈ R ↔ x R y
9 8 pm5.32ri ⊢ C ∈ R ∧ C = x y ↔ x R y ∧ C = x y
10 9 biancomi ⊢ C ∈ R ∧ C = x y ↔ C = x y ∧ x R y
11 10 rexbii ⊢ ∃ y ∈ B C ∈ R ∧ C = x y ↔ ∃ y ∈ B C = x y ∧ x R y
12 11 rexbii ⊢ ∃ x ∈ A ∃ y ∈ B C ∈ R ∧ C = x y ↔ ∃ x ∈ A ∃ y ∈ B C = x y ∧ x R y
13 r19.42v ⊢ ∃ x ∈ A C ∈ R ∧ ∃ y ∈ B C = x y ↔ C ∈ R ∧ ∃ x ∈ A ∃ y ∈ B C = x y
14 5 12 13 3bitr3ri ⊢ C ∈ R ∧ ∃ x ∈ A ∃ y ∈ B C = x y ↔ ∃ x ∈ A ∃ y ∈ B C = x y ∧ x R y
15 1 3 14 3bitri ⊢ C ∈ R ∩ A × B ↔ ∃ x ∈ A ∃ y ∈ B C = x y ∧ x R y