Description: Membership in a Cartesian product. (Contributed by NM, 23-Feb-2004) (Proof shortened by JJ, 13-Aug-2021)
Ref | Expression | ||
---|---|---|---|
Assertion | elxp2 | ⊢ ( 𝐴 ∈ ( 𝐵 × 𝐶 ) ↔ ∃ 𝑥 ∈ 𝐵 ∃ 𝑦 ∈ 𝐶 𝐴 = 〈 𝑥 , 𝑦 〉 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ancom | ⊢ ( ( 𝐴 = 〈 𝑥 , 𝑦 〉 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝐴 = 〈 𝑥 , 𝑦 〉 ) ) | |
2 | 1 | 2exbii | ⊢ ( ∃ 𝑥 ∃ 𝑦 ( 𝐴 = 〈 𝑥 , 𝑦 〉 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) ↔ ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝐴 = 〈 𝑥 , 𝑦 〉 ) ) |
3 | elxp | ⊢ ( 𝐴 ∈ ( 𝐵 × 𝐶 ) ↔ ∃ 𝑥 ∃ 𝑦 ( 𝐴 = 〈 𝑥 , 𝑦 〉 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) ) | |
4 | r2ex | ⊢ ( ∃ 𝑥 ∈ 𝐵 ∃ 𝑦 ∈ 𝐶 𝐴 = 〈 𝑥 , 𝑦 〉 ↔ ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝐴 = 〈 𝑥 , 𝑦 〉 ) ) | |
5 | 2 3 4 | 3bitr4i | ⊢ ( 𝐴 ∈ ( 𝐵 × 𝐶 ) ↔ ∃ 𝑥 ∈ 𝐵 ∃ 𝑦 ∈ 𝐶 𝐴 = 〈 𝑥 , 𝑦 〉 ) |