Step | Hyp | Ref
| Expression |
1 | | elisset 3188 |
. . . 4
⊢ (𝐴 ∈ 𝑉 → ∃𝑦 𝑦 = 𝐴) |
2 | | eleq2 2677 |
. . . . . . 7
⊢ (𝑦 = 𝐴 → ({𝑥} ∈ 𝑦 ↔ {𝑥} ∈ 𝐴)) |
3 | 2 | abbidv 2728 |
. . . . . 6
⊢ (𝑦 = 𝐴 → {𝑥 ∣ {𝑥} ∈ 𝑦} = {𝑥 ∣ {𝑥} ∈ 𝐴}) |
4 | | eleq1 2676 |
. . . . . . 7
⊢ ({𝑥 ∣ {𝑥} ∈ 𝑦} = {𝑥 ∣ {𝑥} ∈ 𝐴} → ({𝑥 ∣ {𝑥} ∈ 𝑦} ∈ V ↔ {𝑥 ∣ {𝑥} ∈ 𝐴} ∈ V)) |
5 | 4 | biimpd 218 |
. . . . . 6
⊢ ({𝑥 ∣ {𝑥} ∈ 𝑦} = {𝑥 ∣ {𝑥} ∈ 𝐴} → ({𝑥 ∣ {𝑥} ∈ 𝑦} ∈ V → {𝑥 ∣ {𝑥} ∈ 𝐴} ∈ V)) |
6 | 3, 5 | syl 17 |
. . . . 5
⊢ (𝑦 = 𝐴 → ({𝑥 ∣ {𝑥} ∈ 𝑦} ∈ V → {𝑥 ∣ {𝑥} ∈ 𝐴} ∈ V)) |
7 | 6 | eximi 1752 |
. . . 4
⊢
(∃𝑦 𝑦 = 𝐴 → ∃𝑦({𝑥 ∣ {𝑥} ∈ 𝑦} ∈ V → {𝑥 ∣ {𝑥} ∈ 𝐴} ∈ V)) |
8 | 1, 7 | syl 17 |
. . 3
⊢ (𝐴 ∈ 𝑉 → ∃𝑦({𝑥 ∣ {𝑥} ∈ 𝑦} ∈ V → {𝑥 ∣ {𝑥} ∈ 𝐴} ∈ V)) |
9 | | 19.35 1794 |
. . . . . 6
⊢
(∃𝑦({𝑥 ∣ {𝑥} ∈ 𝑦} ∈ V → {𝑥 ∣ {𝑥} ∈ 𝐴} ∈ V) ↔ (∀𝑦{𝑥 ∣ {𝑥} ∈ 𝑦} ∈ V → ∃𝑦{𝑥 ∣ {𝑥} ∈ 𝐴} ∈ V)) |
10 | 9 | biimpi 205 |
. . . . 5
⊢
(∃𝑦({𝑥 ∣ {𝑥} ∈ 𝑦} ∈ V → {𝑥 ∣ {𝑥} ∈ 𝐴} ∈ V) → (∀𝑦{𝑥 ∣ {𝑥} ∈ 𝑦} ∈ V → ∃𝑦{𝑥 ∣ {𝑥} ∈ 𝐴} ∈ V)) |
11 | 10 | com12 32 |
. . . 4
⊢
(∀𝑦{𝑥 ∣ {𝑥} ∈ 𝑦} ∈ V → (∃𝑦({𝑥 ∣ {𝑥} ∈ 𝑦} ∈ V → {𝑥 ∣ {𝑥} ∈ 𝐴} ∈ V) → ∃𝑦{𝑥 ∣ {𝑥} ∈ 𝐴} ∈ V)) |
12 | | ax-rep 4699 |
. . . . . . . 8
⊢
(∀𝑢∃𝑧∀𝑡(∀𝑧 𝑢 = {𝑡} → 𝑡 = 𝑧) → ∃𝑧∀𝑡(𝑡 ∈ 𝑧 ↔ ∃𝑢(𝑢 ∈ 𝑦 ∧ ∀𝑧 𝑢 = {𝑡}))) |
13 | | 19.3v 1884 |
. . . . . . . . . . 11
⊢
(∀𝑧 𝑢 = {𝑡} ↔ 𝑢 = {𝑡}) |
14 | 13 | sbbii 1874 |
. . . . . . . . . . 11
⊢ ([𝑧 / 𝑡]∀𝑧 𝑢 = {𝑡} ↔ [𝑧 / 𝑡]𝑢 = {𝑡}) |
15 | | sbsbc 3406 |
. . . . . . . . . . . . . 14
⊢ ([𝑧 / 𝑡]𝑢 = {𝑡} ↔ [𝑧 / 𝑡]𝑢 = {𝑡}) |
16 | | vex 3176 |
. . . . . . . . . . . . . . 15
⊢ 𝑧 ∈ V |
17 | | sbceq2g 3942 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 ∈ V → ([𝑧 / 𝑡]𝑢 = {𝑡} ↔ 𝑢 = ⦋𝑧 / 𝑡⦌{𝑡})) |
18 | 16, 17 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢
([𝑧 / 𝑡]𝑢 = {𝑡} ↔ 𝑢 = ⦋𝑧 / 𝑡⦌{𝑡}) |
19 | 15, 18 | bitri 263 |
. . . . . . . . . . . . 13
⊢ ([𝑧 / 𝑡]𝑢 = {𝑡} ↔ 𝑢 = ⦋𝑧 / 𝑡⦌{𝑡}) |
20 | | bj-csbsn 32091 |
. . . . . . . . . . . . . 14
⊢
⦋𝑧 /
𝑡⦌{𝑡} = {𝑧} |
21 | 20 | eqeq2i 2622 |
. . . . . . . . . . . . 13
⊢ (𝑢 = ⦋𝑧 / 𝑡⦌{𝑡} ↔ 𝑢 = {𝑧}) |
22 | 19, 21 | bitri 263 |
. . . . . . . . . . . 12
⊢ ([𝑧 / 𝑡]𝑢 = {𝑡} ↔ 𝑢 = {𝑧}) |
23 | | eqtr2 2630 |
. . . . . . . . . . . . 13
⊢ ((𝑢 = {𝑡} ∧ 𝑢 = {𝑧}) → {𝑡} = {𝑧}) |
24 | | vex 3176 |
. . . . . . . . . . . . . 14
⊢ 𝑡 ∈ V |
25 | 24 | sneqr 4311 |
. . . . . . . . . . . . 13
⊢ ({𝑡} = {𝑧} → 𝑡 = 𝑧) |
26 | 23, 25 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝑢 = {𝑡} ∧ 𝑢 = {𝑧}) → 𝑡 = 𝑧) |
27 | 22, 26 | sylan2b 491 |
. . . . . . . . . . 11
⊢ ((𝑢 = {𝑡} ∧ [𝑧 / 𝑡]𝑢 = {𝑡}) → 𝑡 = 𝑧) |
28 | 13, 14, 27 | syl2anb 495 |
. . . . . . . . . 10
⊢
((∀𝑧 𝑢 = {𝑡} ∧ [𝑧 / 𝑡]∀𝑧 𝑢 = {𝑡}) → 𝑡 = 𝑧) |
29 | 28 | gen2 1714 |
. . . . . . . . 9
⊢
∀𝑡∀𝑧((∀𝑧 𝑢 = {𝑡} ∧ [𝑧 / 𝑡]∀𝑧 𝑢 = {𝑡}) → 𝑡 = 𝑧) |
30 | | nfa1 2015 |
. . . . . . . . . 10
⊢
Ⅎ𝑧∀𝑧 𝑢 = {𝑡} |
31 | 30 | mo 2496 |
. . . . . . . . 9
⊢
(∃𝑧∀𝑡(∀𝑧 𝑢 = {𝑡} → 𝑡 = 𝑧) ↔ ∀𝑡∀𝑧((∀𝑧 𝑢 = {𝑡} ∧ [𝑧 / 𝑡]∀𝑧 𝑢 = {𝑡}) → 𝑡 = 𝑧)) |
32 | 29, 31 | mpbir 220 |
. . . . . . . 8
⊢
∃𝑧∀𝑡(∀𝑧 𝑢 = {𝑡} → 𝑡 = 𝑧) |
33 | 12, 32 | mpg 1715 |
. . . . . . 7
⊢
∃𝑧∀𝑡(𝑡 ∈ 𝑧 ↔ ∃𝑢(𝑢 ∈ 𝑦 ∧ ∀𝑧 𝑢 = {𝑡})) |
34 | | bj-sbel1 32092 |
. . . . . . . . . . . 12
⊢ ([𝑡 / 𝑥]{𝑥} ∈ 𝑦 ↔ ⦋𝑡 / 𝑥⦌{𝑥} ∈ 𝑦) |
35 | | bj-csbsn 32091 |
. . . . . . . . . . . . 13
⊢
⦋𝑡 /
𝑥⦌{𝑥} = {𝑡} |
36 | 35 | eleq1i 2679 |
. . . . . . . . . . . 12
⊢
(⦋𝑡 /
𝑥⦌{𝑥} ∈ 𝑦 ↔ {𝑡} ∈ 𝑦) |
37 | 34, 36 | bitri 263 |
. . . . . . . . . . 11
⊢ ([𝑡 / 𝑥]{𝑥} ∈ 𝑦 ↔ {𝑡} ∈ 𝑦) |
38 | | df-clab 2597 |
. . . . . . . . . . 11
⊢ (𝑡 ∈ {𝑥 ∣ {𝑥} ∈ 𝑦} ↔ [𝑡 / 𝑥]{𝑥} ∈ 𝑦) |
39 | 13 | anbi2i 726 |
. . . . . . . . . . . . . 14
⊢ ((𝑢 ∈ 𝑦 ∧ ∀𝑧 𝑢 = {𝑡}) ↔ (𝑢 ∈ 𝑦 ∧ 𝑢 = {𝑡})) |
40 | | eleq1a 2683 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑢 ∈ 𝑦 → ({𝑡} = 𝑢 → {𝑡} ∈ 𝑦)) |
41 | 40 | com12 32 |
. . . . . . . . . . . . . . . . 17
⊢ ({𝑡} = 𝑢 → (𝑢 ∈ 𝑦 → {𝑡} ∈ 𝑦)) |
42 | 41 | eqcoms 2618 |
. . . . . . . . . . . . . . . 16
⊢ (𝑢 = {𝑡} → (𝑢 ∈ 𝑦 → {𝑡} ∈ 𝑦)) |
43 | 42 | imdistanri 723 |
. . . . . . . . . . . . . . 15
⊢ ((𝑢 ∈ 𝑦 ∧ 𝑢 = {𝑡}) → ({𝑡} ∈ 𝑦 ∧ 𝑢 = {𝑡})) |
44 | | eleq1a 2683 |
. . . . . . . . . . . . . . . 16
⊢ ({𝑡} ∈ 𝑦 → (𝑢 = {𝑡} → 𝑢 ∈ 𝑦)) |
45 | 44 | impac 649 |
. . . . . . . . . . . . . . 15
⊢ (({𝑡} ∈ 𝑦 ∧ 𝑢 = {𝑡}) → (𝑢 ∈ 𝑦 ∧ 𝑢 = {𝑡})) |
46 | 43, 45 | impbii 198 |
. . . . . . . . . . . . . 14
⊢ ((𝑢 ∈ 𝑦 ∧ 𝑢 = {𝑡}) ↔ ({𝑡} ∈ 𝑦 ∧ 𝑢 = {𝑡})) |
47 | 39, 46 | bitri 263 |
. . . . . . . . . . . . 13
⊢ ((𝑢 ∈ 𝑦 ∧ ∀𝑧 𝑢 = {𝑡}) ↔ ({𝑡} ∈ 𝑦 ∧ 𝑢 = {𝑡})) |
48 | 47 | exbii 1764 |
. . . . . . . . . . . 12
⊢
(∃𝑢(𝑢 ∈ 𝑦 ∧ ∀𝑧 𝑢 = {𝑡}) ↔ ∃𝑢({𝑡} ∈ 𝑦 ∧ 𝑢 = {𝑡})) |
49 | | snex 4835 |
. . . . . . . . . . . . . 14
⊢ {𝑡} ∈ V |
50 | 49 | isseti 3182 |
. . . . . . . . . . . . 13
⊢
∃𝑢 𝑢 = {𝑡} |
51 | | 19.42v 1905 |
. . . . . . . . . . . . 13
⊢
(∃𝑢({𝑡} ∈ 𝑦 ∧ 𝑢 = {𝑡}) ↔ ({𝑡} ∈ 𝑦 ∧ ∃𝑢 𝑢 = {𝑡})) |
52 | 50, 51 | mpbiran2 956 |
. . . . . . . . . . . 12
⊢
(∃𝑢({𝑡} ∈ 𝑦 ∧ 𝑢 = {𝑡}) ↔ {𝑡} ∈ 𝑦) |
53 | 48, 52 | bitri 263 |
. . . . . . . . . . 11
⊢
(∃𝑢(𝑢 ∈ 𝑦 ∧ ∀𝑧 𝑢 = {𝑡}) ↔ {𝑡} ∈ 𝑦) |
54 | 37, 38, 53 | 3bitr4ri 292 |
. . . . . . . . . 10
⊢
(∃𝑢(𝑢 ∈ 𝑦 ∧ ∀𝑧 𝑢 = {𝑡}) ↔ 𝑡 ∈ {𝑥 ∣ {𝑥} ∈ 𝑦}) |
55 | 54 | bibi2i 326 |
. . . . . . . . 9
⊢ ((𝑡 ∈ 𝑧 ↔ ∃𝑢(𝑢 ∈ 𝑦 ∧ ∀𝑧 𝑢 = {𝑡})) ↔ (𝑡 ∈ 𝑧 ↔ 𝑡 ∈ {𝑥 ∣ {𝑥} ∈ 𝑦})) |
56 | 55 | albii 1737 |
. . . . . . . 8
⊢
(∀𝑡(𝑡 ∈ 𝑧 ↔ ∃𝑢(𝑢 ∈ 𝑦 ∧ ∀𝑧 𝑢 = {𝑡})) ↔ ∀𝑡(𝑡 ∈ 𝑧 ↔ 𝑡 ∈ {𝑥 ∣ {𝑥} ∈ 𝑦})) |
57 | 56 | exbii 1764 |
. . . . . . 7
⊢
(∃𝑧∀𝑡(𝑡 ∈ 𝑧 ↔ ∃𝑢(𝑢 ∈ 𝑦 ∧ ∀𝑧 𝑢 = {𝑡})) ↔ ∃𝑧∀𝑡(𝑡 ∈ 𝑧 ↔ 𝑡 ∈ {𝑥 ∣ {𝑥} ∈ 𝑦})) |
58 | 33, 57 | mpbi 219 |
. . . . . 6
⊢
∃𝑧∀𝑡(𝑡 ∈ 𝑧 ↔ 𝑡 ∈ {𝑥 ∣ {𝑥} ∈ 𝑦}) |
59 | | dfcleq 2604 |
. . . . . . 7
⊢ (𝑧 = {𝑥 ∣ {𝑥} ∈ 𝑦} ↔ ∀𝑡(𝑡 ∈ 𝑧 ↔ 𝑡 ∈ {𝑥 ∣ {𝑥} ∈ 𝑦})) |
60 | 59 | exbii 1764 |
. . . . . 6
⊢
(∃𝑧 𝑧 = {𝑥 ∣ {𝑥} ∈ 𝑦} ↔ ∃𝑧∀𝑡(𝑡 ∈ 𝑧 ↔ 𝑡 ∈ {𝑥 ∣ {𝑥} ∈ 𝑦})) |
61 | 58, 60 | mpbir 220 |
. . . . 5
⊢
∃𝑧 𝑧 = {𝑥 ∣ {𝑥} ∈ 𝑦} |
62 | 61 | issetri 3183 |
. . . 4
⊢ {𝑥 ∣ {𝑥} ∈ 𝑦} ∈ V |
63 | 11, 62 | mpg 1715 |
. . 3
⊢
(∃𝑦({𝑥 ∣ {𝑥} ∈ 𝑦} ∈ V → {𝑥 ∣ {𝑥} ∈ 𝐴} ∈ V) → ∃𝑦{𝑥 ∣ {𝑥} ∈ 𝐴} ∈ V) |
64 | 8, 63 | syl 17 |
. 2
⊢ (𝐴 ∈ 𝑉 → ∃𝑦{𝑥 ∣ {𝑥} ∈ 𝐴} ∈ V) |
65 | | ax5e 1829 |
. 2
⊢
(∃𝑦{𝑥 ∣ {𝑥} ∈ 𝐴} ∈ V → {𝑥 ∣ {𝑥} ∈ 𝐴} ∈ V) |
66 | 64, 65 | syl 17 |
1
⊢ (𝐴 ∈ 𝑉 → {𝑥 ∣ {𝑥} ∈ 𝐴} ∈ V) |