Step |
Hyp |
Ref |
Expression |
1 |
|
elxp |
⊢ ( 𝐴 ∈ ( 𝐵 × 𝐶 ) ↔ ∃ 𝑥 ∃ 𝑦 ( 𝐴 = 〈 𝑥 , 𝑦 〉 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) ) |
2 |
|
eqcom |
⊢ ( 〈 𝑥 , 𝑦 〉 = 𝐴 ↔ 𝐴 = 〈 𝑥 , 𝑦 〉 ) |
3 |
|
opelxp |
⊢ ( 〈 𝑥 , 𝑦 〉 ∈ ( 𝐵 × 𝐶 ) ↔ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) |
4 |
2 3
|
anbi12i |
⊢ ( ( 〈 𝑥 , 𝑦 〉 = 𝐴 ∧ 〈 𝑥 , 𝑦 〉 ∈ ( 𝐵 × 𝐶 ) ) ↔ ( 𝐴 = 〈 𝑥 , 𝑦 〉 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) ) |
5 |
4
|
2exbii |
⊢ ( ∃ 𝑥 ∃ 𝑦 ( 〈 𝑥 , 𝑦 〉 = 𝐴 ∧ 〈 𝑥 , 𝑦 〉 ∈ ( 𝐵 × 𝐶 ) ) ↔ ∃ 𝑥 ∃ 𝑦 ( 𝐴 = 〈 𝑥 , 𝑦 〉 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) ) |
6 |
1 5
|
bitr4i |
⊢ ( 𝐴 ∈ ( 𝐵 × 𝐶 ) ↔ ∃ 𝑥 ∃ 𝑦 ( 〈 𝑥 , 𝑦 〉 = 𝐴 ∧ 〈 𝑥 , 𝑦 〉 ∈ ( 𝐵 × 𝐶 ) ) ) |