Step |
Hyp |
Ref |
Expression |
1 |
|
eqeq1 |
⊢ ( 𝑧 = 𝑤 → ( 𝑧 = 〈 𝑥 , 𝑦 〉 ↔ 𝑤 = 〈 𝑥 , 𝑦 〉 ) ) |
2 |
1
|
anbi1d |
⊢ ( 𝑧 = 𝑤 → ( ( 𝑧 = 〈 𝑥 , 𝑦 〉 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) ↔ ( 𝑤 = 〈 𝑥 , 𝑦 〉 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) ) ) |
3 |
2
|
2exbidv |
⊢ ( 𝑧 = 𝑤 → ( ∃ 𝑥 ∃ 𝑦 ( 𝑧 = 〈 𝑥 , 𝑦 〉 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) ↔ ∃ 𝑥 ∃ 𝑦 ( 𝑤 = 〈 𝑥 , 𝑦 〉 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) ) ) |
4 |
|
eqeq1 |
⊢ ( 𝑤 = 𝐴 → ( 𝑤 = 〈 𝑥 , 𝑦 〉 ↔ 𝐴 = 〈 𝑥 , 𝑦 〉 ) ) |
5 |
4
|
anbi1d |
⊢ ( 𝑤 = 𝐴 → ( ( 𝑤 = 〈 𝑥 , 𝑦 〉 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) ↔ ( 𝐴 = 〈 𝑥 , 𝑦 〉 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) ) ) |
6 |
5
|
2exbidv |
⊢ ( 𝑤 = 𝐴 → ( ∃ 𝑥 ∃ 𝑦 ( 𝑤 = 〈 𝑥 , 𝑦 〉 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) ↔ ∃ 𝑥 ∃ 𝑦 ( 𝐴 = 〈 𝑥 , 𝑦 〉 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) ) ) |
7 |
|
df-xp |
⊢ ( 𝐵 × 𝐶 ) = { 〈 𝑥 , 𝑦 〉 ∣ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) } |
8 |
|
df-opab |
⊢ { 〈 𝑥 , 𝑦 〉 ∣ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) } = { 𝑧 ∣ ∃ 𝑥 ∃ 𝑦 ( 𝑧 = 〈 𝑥 , 𝑦 〉 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) } |
9 |
7 8
|
eqtri |
⊢ ( 𝐵 × 𝐶 ) = { 𝑧 ∣ ∃ 𝑥 ∃ 𝑦 ( 𝑧 = 〈 𝑥 , 𝑦 〉 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) } |
10 |
3 6 9
|
elab2gw |
⊢ ( 𝐴 ∈ ( 𝐵 × 𝐶 ) → ( 𝐴 ∈ ( 𝐵 × 𝐶 ) ↔ ∃ 𝑥 ∃ 𝑦 ( 𝐴 = 〈 𝑥 , 𝑦 〉 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) ) ) |
11 |
10
|
ibi |
⊢ ( 𝐴 ∈ ( 𝐵 × 𝐶 ) → ∃ 𝑥 ∃ 𝑦 ( 𝐴 = 〈 𝑥 , 𝑦 〉 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) ) |