Step | Hyp | Ref
| Expression |
1 | | cbvralsvw 3303 |
. 2
⊢
(∀𝑥 ∈
(𝐴 × 𝐵)𝜑 ↔ ∀𝑤 ∈ (𝐴 × 𝐵)[𝑤 / 𝑥]𝜑) |
2 | | cbvralsvw 3303 |
. . . 4
⊢
(∀𝑧 ∈
𝐵 [𝑢 / 𝑦]𝜓 ↔ ∀𝑣 ∈ 𝐵 [𝑣 / 𝑧][𝑢 / 𝑦]𝜓) |
3 | 2 | ralbii 3097 |
. . 3
⊢
(∀𝑢 ∈
𝐴 ∀𝑧 ∈ 𝐵 [𝑢 / 𝑦]𝜓 ↔ ∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐵 [𝑣 / 𝑧][𝑢 / 𝑦]𝜓) |
4 | | nfv 1918 |
. . . 4
⊢
Ⅎ𝑢∀𝑧 ∈ 𝐵 𝜓 |
5 | | nfcv 2908 |
. . . . 5
⊢
Ⅎ𝑦𝐵 |
6 | | nfs1v 2154 |
. . . . 5
⊢
Ⅎ𝑦[𝑢 / 𝑦]𝜓 |
7 | 5, 6 | nfralw 3297 |
. . . 4
⊢
Ⅎ𝑦∀𝑧 ∈ 𝐵 [𝑢 / 𝑦]𝜓 |
8 | | sbequ12 2244 |
. . . . 5
⊢ (𝑦 = 𝑢 → (𝜓 ↔ [𝑢 / 𝑦]𝜓)) |
9 | 8 | ralbidv 3175 |
. . . 4
⊢ (𝑦 = 𝑢 → (∀𝑧 ∈ 𝐵 𝜓 ↔ ∀𝑧 ∈ 𝐵 [𝑢 / 𝑦]𝜓)) |
10 | 4, 7, 9 | cbvralw 3292 |
. . 3
⊢
(∀𝑦 ∈
𝐴 ∀𝑧 ∈ 𝐵 𝜓 ↔ ∀𝑢 ∈ 𝐴 ∀𝑧 ∈ 𝐵 [𝑢 / 𝑦]𝜓) |
11 | | vex 3452 |
. . . . . 6
⊢ 𝑢 ∈ V |
12 | | vex 3452 |
. . . . . 6
⊢ 𝑣 ∈ V |
13 | 11, 12 | eqvinop 5449 |
. . . . 5
⊢ (𝑤 = ⟨𝑢, 𝑣⟩ ↔ ∃𝑦∃𝑧(𝑤 = ⟨𝑦, 𝑧⟩ ∧ ⟨𝑦, 𝑧⟩ = ⟨𝑢, 𝑣⟩)) |
14 | | ralxpf.1 |
. . . . . . . 8
⊢
Ⅎ𝑦𝜑 |
15 | 14 | nfsbv 2324 |
. . . . . . 7
⊢
Ⅎ𝑦[𝑤 / 𝑥]𝜑 |
16 | 6 | nfsbv 2324 |
. . . . . . 7
⊢
Ⅎ𝑦[𝑣 / 𝑧][𝑢 / 𝑦]𝜓 |
17 | 15, 16 | nfbi 1907 |
. . . . . 6
⊢
Ⅎ𝑦([𝑤 / 𝑥]𝜑 ↔ [𝑣 / 𝑧][𝑢 / 𝑦]𝜓) |
18 | | ralxpf.2 |
. . . . . . . . 9
⊢
Ⅎ𝑧𝜑 |
19 | 18 | nfsbv 2324 |
. . . . . . . 8
⊢
Ⅎ𝑧[𝑤 / 𝑥]𝜑 |
20 | | nfs1v 2154 |
. . . . . . . 8
⊢
Ⅎ𝑧[𝑣 / 𝑧][𝑢 / 𝑦]𝜓 |
21 | 19, 20 | nfbi 1907 |
. . . . . . 7
⊢
Ⅎ𝑧([𝑤 / 𝑥]𝜑 ↔ [𝑣 / 𝑧][𝑢 / 𝑦]𝜓) |
22 | | ralxpf.3 |
. . . . . . . . 9
⊢
Ⅎ𝑥𝜓 |
23 | | ralxpf.4 |
. . . . . . . . 9
⊢ (𝑥 = ⟨𝑦, 𝑧⟩ → (𝜑 ↔ 𝜓)) |
24 | 22, 23 | sbhypf 3510 |
. . . . . . . 8
⊢ (𝑤 = ⟨𝑦, 𝑧⟩ → ([𝑤 / 𝑥]𝜑 ↔ 𝜓)) |
25 | | vex 3452 |
. . . . . . . . . 10
⊢ 𝑦 ∈ V |
26 | | vex 3452 |
. . . . . . . . . 10
⊢ 𝑧 ∈ V |
27 | 25, 26 | opth 5438 |
. . . . . . . . 9
⊢
(⟨𝑦, 𝑧⟩ = ⟨𝑢, 𝑣⟩ ↔ (𝑦 = 𝑢 ∧ 𝑧 = 𝑣)) |
28 | | sbequ12 2244 |
. . . . . . . . . 10
⊢ (𝑧 = 𝑣 → ([𝑢 / 𝑦]𝜓 ↔ [𝑣 / 𝑧][𝑢 / 𝑦]𝜓)) |
29 | 8, 28 | sylan9bb 511 |
. . . . . . . . 9
⊢ ((𝑦 = 𝑢 ∧ 𝑧 = 𝑣) → (𝜓 ↔ [𝑣 / 𝑧][𝑢 / 𝑦]𝜓)) |
30 | 27, 29 | sylbi 216 |
. . . . . . . 8
⊢
(⟨𝑦, 𝑧⟩ = ⟨𝑢, 𝑣⟩ → (𝜓 ↔ [𝑣 / 𝑧][𝑢 / 𝑦]𝜓)) |
31 | 24, 30 | sylan9bb 511 |
. . . . . . 7
⊢ ((𝑤 = ⟨𝑦, 𝑧⟩ ∧ ⟨𝑦, 𝑧⟩ = ⟨𝑢, 𝑣⟩) → ([𝑤 / 𝑥]𝜑 ↔ [𝑣 / 𝑧][𝑢 / 𝑦]𝜓)) |
32 | 21, 31 | exlimi 2211 |
. . . . . 6
⊢
(∃𝑧(𝑤 = ⟨𝑦, 𝑧⟩ ∧ ⟨𝑦, 𝑧⟩ = ⟨𝑢, 𝑣⟩) → ([𝑤 / 𝑥]𝜑 ↔ [𝑣 / 𝑧][𝑢 / 𝑦]𝜓)) |
33 | 17, 32 | exlimi 2211 |
. . . . 5
⊢
(∃𝑦∃𝑧(𝑤 = ⟨𝑦, 𝑧⟩ ∧ ⟨𝑦, 𝑧⟩ = ⟨𝑢, 𝑣⟩) → ([𝑤 / 𝑥]𝜑 ↔ [𝑣 / 𝑧][𝑢 / 𝑦]𝜓)) |
34 | 13, 33 | sylbi 216 |
. . . 4
⊢ (𝑤 = ⟨𝑢, 𝑣⟩ → ([𝑤 / 𝑥]𝜑 ↔ [𝑣 / 𝑧][𝑢 / 𝑦]𝜓)) |
35 | 34 | ralxp 5802 |
. . 3
⊢
(∀𝑤 ∈
(𝐴 × 𝐵)[𝑤 / 𝑥]𝜑 ↔ ∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐵 [𝑣 / 𝑧][𝑢 / 𝑦]𝜓) |
36 | 3, 10, 35 | 3bitr4ri 304 |
. 2
⊢
(∀𝑤 ∈
(𝐴 × 𝐵)[𝑤 / 𝑥]𝜑 ↔ ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐵 𝜓) |
37 | 1, 36 | bitri 275 |
1
⊢
(∀𝑥 ∈
(𝐴 × 𝐵)𝜑 ↔ ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐵 𝜓) |