Step | Hyp | Ref
| Expression |
1 | | 19.42v 1958 |
. . . . . . 7
⊢
(∃𝑦(𝑥 ∈ 𝑧 ∧ 𝜑) ↔ (𝑥 ∈ 𝑧 ∧ ∃𝑦𝜑)) |
2 | 1 | abbii 2803 |
. . . . . 6
⊢ {𝑥 ∣ ∃𝑦(𝑥 ∈ 𝑧 ∧ 𝜑)} = {𝑥 ∣ (𝑥 ∈ 𝑧 ∧ ∃𝑦𝜑)} |
3 | | dmopab 5916 |
. . . . . 6
⊢ dom
{⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝑧 ∧ 𝜑)} = {𝑥 ∣ ∃𝑦(𝑥 ∈ 𝑧 ∧ 𝜑)} |
4 | | df-rab 3434 |
. . . . . 6
⊢ {𝑥 ∈ 𝑧 ∣ ∃𝑦𝜑} = {𝑥 ∣ (𝑥 ∈ 𝑧 ∧ ∃𝑦𝜑)} |
5 | 2, 3, 4 | 3eqtr4i 2771 |
. . . . 5
⊢ dom
{⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝑧 ∧ 𝜑)} = {𝑥 ∈ 𝑧 ∣ ∃𝑦𝜑} |
6 | | euex 2572 |
. . . . . . 7
⊢
(∃!𝑦𝜑 → ∃𝑦𝜑) |
7 | 6 | ralimi 3084 |
. . . . . 6
⊢
(∀𝑥 ∈
𝑧 ∃!𝑦𝜑 → ∀𝑥 ∈ 𝑧 ∃𝑦𝜑) |
8 | | rabid2 3465 |
. . . . . 6
⊢ (𝑧 = {𝑥 ∈ 𝑧 ∣ ∃𝑦𝜑} ↔ ∀𝑥 ∈ 𝑧 ∃𝑦𝜑) |
9 | 7, 8 | sylibr 233 |
. . . . 5
⊢
(∀𝑥 ∈
𝑧 ∃!𝑦𝜑 → 𝑧 = {𝑥 ∈ 𝑧 ∣ ∃𝑦𝜑}) |
10 | 5, 9 | eqtr4id 2792 |
. . . 4
⊢
(∀𝑥 ∈
𝑧 ∃!𝑦𝜑 → dom {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝑧 ∧ 𝜑)} = 𝑧) |
11 | | vex 3479 |
. . . 4
⊢ 𝑧 ∈ V |
12 | 10, 11 | eqeltrdi 2842 |
. . 3
⊢
(∀𝑥 ∈
𝑧 ∃!𝑦𝜑 → dom {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝑧 ∧ 𝜑)} ∈ V) |
13 | | eumo 2573 |
. . . . . . 7
⊢
(∃!𝑦𝜑 → ∃*𝑦𝜑) |
14 | 13 | imim2i 16 |
. . . . . 6
⊢ ((𝑥 ∈ 𝑧 → ∃!𝑦𝜑) → (𝑥 ∈ 𝑧 → ∃*𝑦𝜑)) |
15 | | moanimv 2616 |
. . . . . 6
⊢
(∃*𝑦(𝑥 ∈ 𝑧 ∧ 𝜑) ↔ (𝑥 ∈ 𝑧 → ∃*𝑦𝜑)) |
16 | 14, 15 | sylibr 233 |
. . . . 5
⊢ ((𝑥 ∈ 𝑧 → ∃!𝑦𝜑) → ∃*𝑦(𝑥 ∈ 𝑧 ∧ 𝜑)) |
17 | 16 | alimi 1814 |
. . . 4
⊢
(∀𝑥(𝑥 ∈ 𝑧 → ∃!𝑦𝜑) → ∀𝑥∃*𝑦(𝑥 ∈ 𝑧 ∧ 𝜑)) |
18 | | df-ral 3063 |
. . . 4
⊢
(∀𝑥 ∈
𝑧 ∃!𝑦𝜑 ↔ ∀𝑥(𝑥 ∈ 𝑧 → ∃!𝑦𝜑)) |
19 | | funopab 6584 |
. . . 4
⊢ (Fun
{⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝑧 ∧ 𝜑)} ↔ ∀𝑥∃*𝑦(𝑥 ∈ 𝑧 ∧ 𝜑)) |
20 | 17, 18, 19 | 3imtr4i 292 |
. . 3
⊢
(∀𝑥 ∈
𝑧 ∃!𝑦𝜑 → Fun {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝑧 ∧ 𝜑)}) |
21 | | funrnex 7940 |
. . 3
⊢ (dom
{⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝑧 ∧ 𝜑)} ∈ V → (Fun {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝑧 ∧ 𝜑)} → ran {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝑧 ∧ 𝜑)} ∈ V)) |
22 | 12, 20, 21 | sylc 65 |
. 2
⊢
(∀𝑥 ∈
𝑧 ∃!𝑦𝜑 → ran {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝑧 ∧ 𝜑)} ∈ V) |
23 | | nfra1 3282 |
. . 3
⊢
Ⅎ𝑥∀𝑥 ∈ 𝑧 ∃!𝑦𝜑 |
24 | 10 | eleq2d 2820 |
. . . 4
⊢
(∀𝑥 ∈
𝑧 ∃!𝑦𝜑 → (𝑥 ∈ dom {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝑧 ∧ 𝜑)} ↔ 𝑥 ∈ 𝑧)) |
25 | | opabidw 5525 |
. . . . . . . . 9
⊢
(⟨𝑥, 𝑦⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝑧 ∧ 𝜑)} ↔ (𝑥 ∈ 𝑧 ∧ 𝜑)) |
26 | | vex 3479 |
. . . . . . . . . 10
⊢ 𝑥 ∈ V |
27 | | vex 3479 |
. . . . . . . . . 10
⊢ 𝑦 ∈ V |
28 | 26, 27 | opelrn 5943 |
. . . . . . . . 9
⊢
(⟨𝑥, 𝑦⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝑧 ∧ 𝜑)} → 𝑦 ∈ ran {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝑧 ∧ 𝜑)}) |
29 | 25, 28 | sylbir 234 |
. . . . . . . 8
⊢ ((𝑥 ∈ 𝑧 ∧ 𝜑) → 𝑦 ∈ ran {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝑧 ∧ 𝜑)}) |
30 | 29 | ex 414 |
. . . . . . 7
⊢ (𝑥 ∈ 𝑧 → (𝜑 → 𝑦 ∈ ran {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝑧 ∧ 𝜑)})) |
31 | 30 | impac 554 |
. . . . . 6
⊢ ((𝑥 ∈ 𝑧 ∧ 𝜑) → (𝑦 ∈ ran {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝑧 ∧ 𝜑)} ∧ 𝜑)) |
32 | 31 | eximi 1838 |
. . . . 5
⊢
(∃𝑦(𝑥 ∈ 𝑧 ∧ 𝜑) → ∃𝑦(𝑦 ∈ ran {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝑧 ∧ 𝜑)} ∧ 𝜑)) |
33 | 3 | eqabri 2878 |
. . . . 5
⊢ (𝑥 ∈ dom {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝑧 ∧ 𝜑)} ↔ ∃𝑦(𝑥 ∈ 𝑧 ∧ 𝜑)) |
34 | | df-rex 3072 |
. . . . 5
⊢
(∃𝑦 ∈ ran
{⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝑧 ∧ 𝜑)}𝜑 ↔ ∃𝑦(𝑦 ∈ ran {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝑧 ∧ 𝜑)} ∧ 𝜑)) |
35 | 32, 33, 34 | 3imtr4i 292 |
. . . 4
⊢ (𝑥 ∈ dom {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝑧 ∧ 𝜑)} → ∃𝑦 ∈ ran {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝑧 ∧ 𝜑)}𝜑) |
36 | 24, 35 | syl6bir 254 |
. . 3
⊢
(∀𝑥 ∈
𝑧 ∃!𝑦𝜑 → (𝑥 ∈ 𝑧 → ∃𝑦 ∈ ran {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝑧 ∧ 𝜑)}𝜑)) |
37 | 23, 36 | ralrimi 3255 |
. 2
⊢
(∀𝑥 ∈
𝑧 ∃!𝑦𝜑 → ∀𝑥 ∈ 𝑧 ∃𝑦 ∈ ran {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝑧 ∧ 𝜑)}𝜑) |
38 | | nfopab1 5219 |
. . . . 5
⊢
Ⅎ𝑥{⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝑧 ∧ 𝜑)} |
39 | 38 | nfrn 5952 |
. . . 4
⊢
Ⅎ𝑥ran
{⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝑧 ∧ 𝜑)} |
40 | 39 | nfeq2 2921 |
. . 3
⊢
Ⅎ𝑥 𝑤 = ran {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝑧 ∧ 𝜑)} |
41 | | nfcv 2904 |
. . . 4
⊢
Ⅎ𝑦𝑤 |
42 | | nfopab2 5220 |
. . . . 5
⊢
Ⅎ𝑦{⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝑧 ∧ 𝜑)} |
43 | 42 | nfrn 5952 |
. . . 4
⊢
Ⅎ𝑦ran
{⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝑧 ∧ 𝜑)} |
44 | 41, 43 | rexeqf 3351 |
. . 3
⊢ (𝑤 = ran {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝑧 ∧ 𝜑)} → (∃𝑦 ∈ 𝑤 𝜑 ↔ ∃𝑦 ∈ ran {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝑧 ∧ 𝜑)}𝜑)) |
45 | 40, 44 | ralbid 3271 |
. 2
⊢ (𝑤 = ran {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝑧 ∧ 𝜑)} → (∀𝑥 ∈ 𝑧 ∃𝑦 ∈ 𝑤 𝜑 ↔ ∀𝑥 ∈ 𝑧 ∃𝑦 ∈ ran {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝑧 ∧ 𝜑)}𝜑)) |
46 | 22, 37, 45 | spcedv 3589 |
1
⊢
(∀𝑥 ∈
𝑧 ∃!𝑦𝜑 → ∃𝑤∀𝑥 ∈ 𝑧 ∃𝑦 ∈ 𝑤 𝜑) |