Step | Hyp | Ref
| Expression |
1 | | simplr 768 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 = 𝑤) ∧ 𝑧 = 𝑣) → 𝑥 = 𝑤) |
2 | | eqidd 2734 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 = 𝑤) ∧ 𝑧 = 𝑣) → 𝑦 = 𝑦) |
3 | 1, 2 | opeq12d 4888 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 = 𝑤) ∧ 𝑧 = 𝑣) → 〈𝑥, 𝑦〉 = 〈𝑤, 𝑦〉) |
4 | | simpr 484 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 = 𝑤) ∧ 𝑧 = 𝑣) → 𝑧 = 𝑣) |
5 | 3, 4 | opeq12d 4888 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 = 𝑤) ∧ 𝑧 = 𝑣) → 〈〈𝑥, 𝑦〉, 𝑧〉 = 〈〈𝑤, 𝑦〉, 𝑣〉) |
6 | 5 | eqeq2d 2744 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 = 𝑤) ∧ 𝑧 = 𝑣) → (𝑡 = 〈〈𝑥, 𝑦〉, 𝑧〉 ↔ 𝑡 = 〈〈𝑤, 𝑦〉, 𝑣〉)) |
7 | | cbvoprab13davw.1 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 = 𝑤) ∧ 𝑧 = 𝑣) → (𝜓 ↔ 𝜒)) |
8 | 6, 7 | anbi12d 631 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 = 𝑤) ∧ 𝑧 = 𝑣) → ((𝑡 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜓) ↔ (𝑡 = 〈〈𝑤, 𝑦〉, 𝑣〉 ∧ 𝜒))) |
9 | 8 | cbvexdvaw 2034 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 = 𝑤) → (∃𝑧(𝑡 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜓) ↔ ∃𝑣(𝑡 = 〈〈𝑤, 𝑦〉, 𝑣〉 ∧ 𝜒))) |
10 | 9 | exbidv 1917 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 = 𝑤) → (∃𝑦∃𝑧(𝑡 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜓) ↔ ∃𝑦∃𝑣(𝑡 = 〈〈𝑤, 𝑦〉, 𝑣〉 ∧ 𝜒))) |
11 | 10 | cbvexdvaw 2034 |
. . 3
⊢ (𝜑 → (∃𝑥∃𝑦∃𝑧(𝑡 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜓) ↔ ∃𝑤∃𝑦∃𝑣(𝑡 = 〈〈𝑤, 𝑦〉, 𝑣〉 ∧ 𝜒))) |
12 | 11 | abbidv 2804 |
. 2
⊢ (𝜑 → {𝑡 ∣ ∃𝑥∃𝑦∃𝑧(𝑡 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜓)} = {𝑡 ∣ ∃𝑤∃𝑦∃𝑣(𝑡 = 〈〈𝑤, 𝑦〉, 𝑣〉 ∧ 𝜒)}) |
13 | | df-oprab 7429 |
. 2
⊢
{〈〈𝑥,
𝑦〉, 𝑧〉 ∣ 𝜓} = {𝑡 ∣ ∃𝑥∃𝑦∃𝑧(𝑡 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜓)} |
14 | | df-oprab 7429 |
. 2
⊢
{〈〈𝑤,
𝑦〉, 𝑣〉 ∣ 𝜒} = {𝑡 ∣ ∃𝑤∃𝑦∃𝑣(𝑡 = 〈〈𝑤, 𝑦〉, 𝑣〉 ∧ 𝜒)} |
15 | 12, 13, 14 | 3eqtr4g 2798 |
1
⊢ (𝜑 → {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜓} = {〈〈𝑤, 𝑦〉, 𝑣〉 ∣ 𝜒}) |