Step |
Hyp |
Ref |
Expression |
1 |
|
biidd |
⊢ ( 𝑢 = 〈 𝑥 , 𝑦 〉 → ( 𝑧 ∈ 𝐶 ↔ 𝑧 ∈ 𝐶 ) ) |
2 |
1
|
dfoprab4 |
⊢ { 〈 𝑢 , 𝑧 〉 ∣ ( 𝑢 ∈ ( 𝐴 × 𝐵 ) ∧ 𝑧 ∈ 𝐶 ) } = { 〈 〈 𝑥 , 𝑦 〉 , 𝑧 〉 ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 ∈ 𝐶 ) } |
3 |
|
df-xp |
⊢ ( ( 𝐴 × 𝐵 ) × 𝐶 ) = { 〈 𝑢 , 𝑧 〉 ∣ ( 𝑢 ∈ ( 𝐴 × 𝐵 ) ∧ 𝑧 ∈ 𝐶 ) } |
4 |
|
df-3an |
⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶 ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 ∈ 𝐶 ) ) |
5 |
4
|
oprabbii |
⊢ { 〈 〈 𝑥 , 𝑦 〉 , 𝑧 〉 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶 ) } = { 〈 〈 𝑥 , 𝑦 〉 , 𝑧 〉 ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 ∈ 𝐶 ) } |
6 |
2 3 5
|
3eqtr4i |
⊢ ( ( 𝐴 × 𝐵 ) × 𝐶 ) = { 〈 〈 𝑥 , 𝑦 〉 , 𝑧 〉 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶 ) } |