Step |
Hyp |
Ref |
Expression |
1 |
|
elxp2 |
⊢ ( 𝐴 ∈ ( ( 𝐵 × 𝐶 ) × 𝐷 ) ↔ ∃ 𝑝 ∈ ( 𝐵 × 𝐶 ) ∃ 𝑧 ∈ 𝐷 𝐴 = ⟨ 𝑝 , 𝑧 ⟩ ) |
2 |
|
opeq1 |
⊢ ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ → ⟨ 𝑝 , 𝑧 ⟩ = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ) |
3 |
2
|
eqeq2d |
⊢ ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝐴 = ⟨ 𝑝 , 𝑧 ⟩ ↔ 𝐴 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ) ) |
4 |
3
|
rexbidv |
⊢ ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ → ( ∃ 𝑧 ∈ 𝐷 𝐴 = ⟨ 𝑝 , 𝑧 ⟩ ↔ ∃ 𝑧 ∈ 𝐷 𝐴 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ) ) |
5 |
4
|
rexxp |
⊢ ( ∃ 𝑝 ∈ ( 𝐵 × 𝐶 ) ∃ 𝑧 ∈ 𝐷 𝐴 = ⟨ 𝑝 , 𝑧 ⟩ ↔ ∃ 𝑥 ∈ 𝐵 ∃ 𝑦 ∈ 𝐶 ∃ 𝑧 ∈ 𝐷 𝐴 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ) |
6 |
|
df-ot |
⊢ ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ |
7 |
6
|
eqcomi |
⊢ ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ |
8 |
7
|
eqeq2i |
⊢ ( 𝐴 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ↔ 𝐴 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ) |
9 |
8
|
rexbii |
⊢ ( ∃ 𝑧 ∈ 𝐷 𝐴 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ↔ ∃ 𝑧 ∈ 𝐷 𝐴 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ) |
10 |
9
|
rexbii |
⊢ ( ∃ 𝑦 ∈ 𝐶 ∃ 𝑧 ∈ 𝐷 𝐴 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ↔ ∃ 𝑦 ∈ 𝐶 ∃ 𝑧 ∈ 𝐷 𝐴 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ) |
11 |
10
|
rexbii |
⊢ ( ∃ 𝑥 ∈ 𝐵 ∃ 𝑦 ∈ 𝐶 ∃ 𝑧 ∈ 𝐷 𝐴 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ↔ ∃ 𝑥 ∈ 𝐵 ∃ 𝑦 ∈ 𝐶 ∃ 𝑧 ∈ 𝐷 𝐴 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ) |
12 |
1 5 11
|
3bitri |
⊢ ( 𝐴 ∈ ( ( 𝐵 × 𝐶 ) × 𝐷 ) ↔ ∃ 𝑥 ∈ 𝐵 ∃ 𝑦 ∈ 𝐶 ∃ 𝑧 ∈ 𝐷 𝐴 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ) |