Step | Hyp | Ref
| Expression |
1 | | cbvralsvw 3368 |
. 2
⊢
(∀𝑥 ∈
(𝐴 × 𝐵)𝜑 ↔ ∀𝑤 ∈ (𝐴 × 𝐵)[𝑤 / 𝑥]𝜑) |
2 | | cbvralsvw 3368 |
. . . 4
⊢
(∀𝑧 ∈
𝐵 [𝑢 / 𝑦]𝜓 ↔ ∀𝑣 ∈ 𝐵 [𝑣 / 𝑧][𝑢 / 𝑦]𝜓) |
3 | 2 | ralbii 3080 |
. . 3
⊢
(∀𝑢 ∈
𝐴 ∀𝑧 ∈ 𝐵 [𝑢 / 𝑦]𝜓 ↔ ∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐵 [𝑣 / 𝑧][𝑢 / 𝑦]𝜓) |
4 | | nfv 1921 |
. . . 4
⊢
Ⅎ𝑢∀𝑧 ∈ 𝐵 𝜓 |
5 | | nfcv 2899 |
. . . . 5
⊢
Ⅎ𝑦𝐵 |
6 | | nfs1v 2161 |
. . . . 5
⊢
Ⅎ𝑦[𝑢 / 𝑦]𝜓 |
7 | 5, 6 | nfralw 3138 |
. . . 4
⊢
Ⅎ𝑦∀𝑧 ∈ 𝐵 [𝑢 / 𝑦]𝜓 |
8 | | sbequ12 2253 |
. . . . 5
⊢ (𝑦 = 𝑢 → (𝜓 ↔ [𝑢 / 𝑦]𝜓)) |
9 | 8 | ralbidv 3109 |
. . . 4
⊢ (𝑦 = 𝑢 → (∀𝑧 ∈ 𝐵 𝜓 ↔ ∀𝑧 ∈ 𝐵 [𝑢 / 𝑦]𝜓)) |
10 | 4, 7, 9 | cbvralw 3340 |
. . 3
⊢
(∀𝑦 ∈
𝐴 ∀𝑧 ∈ 𝐵 𝜓 ↔ ∀𝑢 ∈ 𝐴 ∀𝑧 ∈ 𝐵 [𝑢 / 𝑦]𝜓) |
11 | | vex 3402 |
. . . . . 6
⊢ 𝑢 ∈ V |
12 | | vex 3402 |
. . . . . 6
⊢ 𝑣 ∈ V |
13 | 11, 12 | eqvinop 5344 |
. . . . 5
⊢ (𝑤 = 〈𝑢, 𝑣〉 ↔ ∃𝑦∃𝑧(𝑤 = 〈𝑦, 𝑧〉 ∧ 〈𝑦, 𝑧〉 = 〈𝑢, 𝑣〉)) |
14 | | ralxpf.1 |
. . . . . . . 8
⊢
Ⅎ𝑦𝜑 |
15 | 14 | nfsbv 2332 |
. . . . . . 7
⊢
Ⅎ𝑦[𝑤 / 𝑥]𝜑 |
16 | 6 | nfsbv 2332 |
. . . . . . 7
⊢
Ⅎ𝑦[𝑣 / 𝑧][𝑢 / 𝑦]𝜓 |
17 | 15, 16 | nfbi 1910 |
. . . . . 6
⊢
Ⅎ𝑦([𝑤 / 𝑥]𝜑 ↔ [𝑣 / 𝑧][𝑢 / 𝑦]𝜓) |
18 | | ralxpf.2 |
. . . . . . . . 9
⊢
Ⅎ𝑧𝜑 |
19 | 18 | nfsbv 2332 |
. . . . . . . 8
⊢
Ⅎ𝑧[𝑤 / 𝑥]𝜑 |
20 | | nfs1v 2161 |
. . . . . . . 8
⊢
Ⅎ𝑧[𝑣 / 𝑧][𝑢 / 𝑦]𝜓 |
21 | 19, 20 | nfbi 1910 |
. . . . . . 7
⊢
Ⅎ𝑧([𝑤 / 𝑥]𝜑 ↔ [𝑣 / 𝑧][𝑢 / 𝑦]𝜓) |
22 | | ralxpf.3 |
. . . . . . . . 9
⊢
Ⅎ𝑥𝜓 |
23 | | ralxpf.4 |
. . . . . . . . 9
⊢ (𝑥 = 〈𝑦, 𝑧〉 → (𝜑 ↔ 𝜓)) |
24 | 22, 23 | sbhypf 3456 |
. . . . . . . 8
⊢ (𝑤 = 〈𝑦, 𝑧〉 → ([𝑤 / 𝑥]𝜑 ↔ 𝜓)) |
25 | | vex 3402 |
. . . . . . . . . 10
⊢ 𝑦 ∈ V |
26 | | vex 3402 |
. . . . . . . . . 10
⊢ 𝑧 ∈ V |
27 | 25, 26 | opth 5334 |
. . . . . . . . 9
⊢
(〈𝑦, 𝑧〉 = 〈𝑢, 𝑣〉 ↔ (𝑦 = 𝑢 ∧ 𝑧 = 𝑣)) |
28 | | sbequ12 2253 |
. . . . . . . . . 10
⊢ (𝑧 = 𝑣 → ([𝑢 / 𝑦]𝜓 ↔ [𝑣 / 𝑧][𝑢 / 𝑦]𝜓)) |
29 | 8, 28 | sylan9bb 513 |
. . . . . . . . 9
⊢ ((𝑦 = 𝑢 ∧ 𝑧 = 𝑣) → (𝜓 ↔ [𝑣 / 𝑧][𝑢 / 𝑦]𝜓)) |
30 | 27, 29 | sylbi 220 |
. . . . . . . 8
⊢
(〈𝑦, 𝑧〉 = 〈𝑢, 𝑣〉 → (𝜓 ↔ [𝑣 / 𝑧][𝑢 / 𝑦]𝜓)) |
31 | 24, 30 | sylan9bb 513 |
. . . . . . 7
⊢ ((𝑤 = 〈𝑦, 𝑧〉 ∧ 〈𝑦, 𝑧〉 = 〈𝑢, 𝑣〉) → ([𝑤 / 𝑥]𝜑 ↔ [𝑣 / 𝑧][𝑢 / 𝑦]𝜓)) |
32 | 21, 31 | exlimi 2219 |
. . . . . 6
⊢
(∃𝑧(𝑤 = 〈𝑦, 𝑧〉 ∧ 〈𝑦, 𝑧〉 = 〈𝑢, 𝑣〉) → ([𝑤 / 𝑥]𝜑 ↔ [𝑣 / 𝑧][𝑢 / 𝑦]𝜓)) |
33 | 17, 32 | exlimi 2219 |
. . . . 5
⊢
(∃𝑦∃𝑧(𝑤 = 〈𝑦, 𝑧〉 ∧ 〈𝑦, 𝑧〉 = 〈𝑢, 𝑣〉) → ([𝑤 / 𝑥]𝜑 ↔ [𝑣 / 𝑧][𝑢 / 𝑦]𝜓)) |
34 | 13, 33 | sylbi 220 |
. . . 4
⊢ (𝑤 = 〈𝑢, 𝑣〉 → ([𝑤 / 𝑥]𝜑 ↔ [𝑣 / 𝑧][𝑢 / 𝑦]𝜓)) |
35 | 34 | ralxp 5684 |
. . 3
⊢
(∀𝑤 ∈
(𝐴 × 𝐵)[𝑤 / 𝑥]𝜑 ↔ ∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐵 [𝑣 / 𝑧][𝑢 / 𝑦]𝜓) |
36 | 3, 10, 35 | 3bitr4ri 307 |
. 2
⊢
(∀𝑤 ∈
(𝐴 × 𝐵)[𝑤 / 𝑥]𝜑 ↔ ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐵 𝜓) |
37 | 1, 36 | bitri 278 |
1
⊢
(∀𝑥 ∈
(𝐴 × 𝐵)𝜑 ↔ ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐵 𝜓) |