Step | Hyp | Ref
| Expression |
1 | | elisset 2808 |
. 2
⊢ (𝐴 ∈ 𝑉 → ∃𝑦 𝑦 = 𝐴) |
2 | | eleq2 2815 |
. . . . 5
⊢ (𝑦 = 𝐴 → ({𝑥} ∈ 𝑦 ↔ {𝑥} ∈ 𝐴)) |
3 | 2 | abbidv 2795 |
. . . 4
⊢ (𝑦 = 𝐴 → {𝑥 ∣ {𝑥} ∈ 𝑦} = {𝑥 ∣ {𝑥} ∈ 𝐴}) |
4 | | eleq1 2814 |
. . . . 5
⊢ ({𝑥 ∣ {𝑥} ∈ 𝑦} = {𝑥 ∣ {𝑥} ∈ 𝐴} → ({𝑥 ∣ {𝑥} ∈ 𝑦} ∈ V ↔ {𝑥 ∣ {𝑥} ∈ 𝐴} ∈ V)) |
5 | 4 | biimpd 228 |
. . . 4
⊢ ({𝑥 ∣ {𝑥} ∈ 𝑦} = {𝑥 ∣ {𝑥} ∈ 𝐴} → ({𝑥 ∣ {𝑥} ∈ 𝑦} ∈ V → {𝑥 ∣ {𝑥} ∈ 𝐴} ∈ V)) |
6 | 3, 5 | syl 17 |
. . 3
⊢ (𝑦 = 𝐴 → ({𝑥 ∣ {𝑥} ∈ 𝑦} ∈ V → {𝑥 ∣ {𝑥} ∈ 𝐴} ∈ V)) |
7 | 6 | eximi 1830 |
. 2
⊢
(∃𝑦 𝑦 = 𝐴 → ∃𝑦({𝑥 ∣ {𝑥} ∈ 𝑦} ∈ V → {𝑥 ∣ {𝑥} ∈ 𝐴} ∈ V)) |
8 | | bj-eximcom 36360 |
. . . 4
⊢
(∃𝑦({𝑥 ∣ {𝑥} ∈ 𝑦} ∈ V → {𝑥 ∣ {𝑥} ∈ 𝐴} ∈ V) → (∀𝑦{𝑥 ∣ {𝑥} ∈ 𝑦} ∈ V → ∃𝑦{𝑥 ∣ {𝑥} ∈ 𝐴} ∈ V)) |
9 | 8 | com12 32 |
. . 3
⊢
(∀𝑦{𝑥 ∣ {𝑥} ∈ 𝑦} ∈ V → (∃𝑦({𝑥 ∣ {𝑥} ∈ 𝑦} ∈ V → {𝑥 ∣ {𝑥} ∈ 𝐴} ∈ V) → ∃𝑦{𝑥 ∣ {𝑥} ∈ 𝐴} ∈ V)) |
10 | | ax-rep 5282 |
. . . . . . 7
⊢
(∀𝑢∃𝑧∀𝑡(∀𝑧 𝑢 = {𝑡} → 𝑡 = 𝑧) → ∃𝑧∀𝑡(𝑡 ∈ 𝑧 ↔ ∃𝑢(𝑢 ∈ 𝑦 ∧ ∀𝑧 𝑢 = {𝑡}))) |
11 | | 19.3v 1978 |
. . . . . . . . . 10
⊢
(∀𝑧 𝑢 = {𝑡} ↔ 𝑢 = {𝑡}) |
12 | 11 | sbbii 2072 |
. . . . . . . . . 10
⊢ ([𝑧 / 𝑡]∀𝑧 𝑢 = {𝑡} ↔ [𝑧 / 𝑡]𝑢 = {𝑡}) |
13 | | sbsbc 3779 |
. . . . . . . . . . . . 13
⊢ ([𝑧 / 𝑡]𝑢 = {𝑡} ↔ [𝑧 / 𝑡]𝑢 = {𝑡}) |
14 | | sbceq2g 4413 |
. . . . . . . . . . . . . 14
⊢ (𝑧 ∈ V → ([𝑧 / 𝑡]𝑢 = {𝑡} ↔ 𝑢 = ⦋𝑧 / 𝑡⦌{𝑡})) |
15 | 14 | elv 3468 |
. . . . . . . . . . . . 13
⊢
([𝑧 / 𝑡]𝑢 = {𝑡} ↔ 𝑢 = ⦋𝑧 / 𝑡⦌{𝑡}) |
16 | 13, 15 | bitri 274 |
. . . . . . . . . . . 12
⊢ ([𝑧 / 𝑡]𝑢 = {𝑡} ↔ 𝑢 = ⦋𝑧 / 𝑡⦌{𝑡}) |
17 | | bj-csbsn 36623 |
. . . . . . . . . . . . 13
⊢
⦋𝑧 /
𝑡⦌{𝑡} = {𝑧} |
18 | 17 | eqeq2i 2739 |
. . . . . . . . . . . 12
⊢ (𝑢 = ⦋𝑧 / 𝑡⦌{𝑡} ↔ 𝑢 = {𝑧}) |
19 | 16, 18 | bitri 274 |
. . . . . . . . . . 11
⊢ ([𝑧 / 𝑡]𝑢 = {𝑡} ↔ 𝑢 = {𝑧}) |
20 | | eqtr2 2750 |
. . . . . . . . . . . 12
⊢ ((𝑢 = {𝑡} ∧ 𝑢 = {𝑧}) → {𝑡} = {𝑧}) |
21 | | vex 3466 |
. . . . . . . . . . . . 13
⊢ 𝑡 ∈ V |
22 | 21 | sneqr 4839 |
. . . . . . . . . . . 12
⊢ ({𝑡} = {𝑧} → 𝑡 = 𝑧) |
23 | 20, 22 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝑢 = {𝑡} ∧ 𝑢 = {𝑧}) → 𝑡 = 𝑧) |
24 | 19, 23 | sylan2b 592 |
. . . . . . . . . 10
⊢ ((𝑢 = {𝑡} ∧ [𝑧 / 𝑡]𝑢 = {𝑡}) → 𝑡 = 𝑧) |
25 | 11, 12, 24 | syl2anb 596 |
. . . . . . . . 9
⊢
((∀𝑧 𝑢 = {𝑡} ∧ [𝑧 / 𝑡]∀𝑧 𝑢 = {𝑡}) → 𝑡 = 𝑧) |
26 | 25 | gen2 1791 |
. . . . . . . 8
⊢
∀𝑡∀𝑧((∀𝑧 𝑢 = {𝑡} ∧ [𝑧 / 𝑡]∀𝑧 𝑢 = {𝑡}) → 𝑡 = 𝑧) |
27 | | nfa1 2141 |
. . . . . . . . 9
⊢
Ⅎ𝑧∀𝑧 𝑢 = {𝑡} |
28 | 27 | mo 2554 |
. . . . . . . 8
⊢
(∃𝑧∀𝑡(∀𝑧 𝑢 = {𝑡} → 𝑡 = 𝑧) ↔ ∀𝑡∀𝑧((∀𝑧 𝑢 = {𝑡} ∧ [𝑧 / 𝑡]∀𝑧 𝑢 = {𝑡}) → 𝑡 = 𝑧)) |
29 | 26, 28 | mpbir 230 |
. . . . . . 7
⊢
∃𝑧∀𝑡(∀𝑧 𝑢 = {𝑡} → 𝑡 = 𝑧) |
30 | 10, 29 | mpg 1792 |
. . . . . 6
⊢
∃𝑧∀𝑡(𝑡 ∈ 𝑧 ↔ ∃𝑢(𝑢 ∈ 𝑦 ∧ ∀𝑧 𝑢 = {𝑡})) |
31 | | bj-sbel1 36624 |
. . . . . . . . . . 11
⊢ ([𝑡 / 𝑥]{𝑥} ∈ 𝑦 ↔ ⦋𝑡 / 𝑥⦌{𝑥} ∈ 𝑦) |
32 | | bj-csbsn 36623 |
. . . . . . . . . . . 12
⊢
⦋𝑡 /
𝑥⦌{𝑥} = {𝑡} |
33 | 32 | eleq1i 2817 |
. . . . . . . . . . 11
⊢
(⦋𝑡 /
𝑥⦌{𝑥} ∈ 𝑦 ↔ {𝑡} ∈ 𝑦) |
34 | 31, 33 | bitri 274 |
. . . . . . . . . 10
⊢ ([𝑡 / 𝑥]{𝑥} ∈ 𝑦 ↔ {𝑡} ∈ 𝑦) |
35 | | df-clab 2704 |
. . . . . . . . . 10
⊢ (𝑡 ∈ {𝑥 ∣ {𝑥} ∈ 𝑦} ↔ [𝑡 / 𝑥]{𝑥} ∈ 𝑦) |
36 | 11 | anbi2i 621 |
. . . . . . . . . . . . 13
⊢ ((𝑢 ∈ 𝑦 ∧ ∀𝑧 𝑢 = {𝑡}) ↔ (𝑢 ∈ 𝑦 ∧ 𝑢 = {𝑡})) |
37 | | eleq1a 2821 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑢 ∈ 𝑦 → ({𝑡} = 𝑢 → {𝑡} ∈ 𝑦)) |
38 | 37 | com12 32 |
. . . . . . . . . . . . . . . 16
⊢ ({𝑡} = 𝑢 → (𝑢 ∈ 𝑦 → {𝑡} ∈ 𝑦)) |
39 | 38 | eqcoms 2734 |
. . . . . . . . . . . . . . 15
⊢ (𝑢 = {𝑡} → (𝑢 ∈ 𝑦 → {𝑡} ∈ 𝑦)) |
40 | 39 | imdistanri 568 |
. . . . . . . . . . . . . 14
⊢ ((𝑢 ∈ 𝑦 ∧ 𝑢 = {𝑡}) → ({𝑡} ∈ 𝑦 ∧ 𝑢 = {𝑡})) |
41 | | eleq1a 2821 |
. . . . . . . . . . . . . . 15
⊢ ({𝑡} ∈ 𝑦 → (𝑢 = {𝑡} → 𝑢 ∈ 𝑦)) |
42 | 41 | impac 551 |
. . . . . . . . . . . . . 14
⊢ (({𝑡} ∈ 𝑦 ∧ 𝑢 = {𝑡}) → (𝑢 ∈ 𝑦 ∧ 𝑢 = {𝑡})) |
43 | 40, 42 | impbii 208 |
. . . . . . . . . . . . 13
⊢ ((𝑢 ∈ 𝑦 ∧ 𝑢 = {𝑡}) ↔ ({𝑡} ∈ 𝑦 ∧ 𝑢 = {𝑡})) |
44 | 36, 43 | bitri 274 |
. . . . . . . . . . . 12
⊢ ((𝑢 ∈ 𝑦 ∧ ∀𝑧 𝑢 = {𝑡}) ↔ ({𝑡} ∈ 𝑦 ∧ 𝑢 = {𝑡})) |
45 | 44 | exbii 1843 |
. . . . . . . . . . 11
⊢
(∃𝑢(𝑢 ∈ 𝑦 ∧ ∀𝑧 𝑢 = {𝑡}) ↔ ∃𝑢({𝑡} ∈ 𝑦 ∧ 𝑢 = {𝑡})) |
46 | | vsnex 5427 |
. . . . . . . . . . . . 13
⊢ {𝑡} ∈ V |
47 | 46 | isseti 3479 |
. . . . . . . . . . . 12
⊢
∃𝑢 𝑢 = {𝑡} |
48 | | 19.42v 1950 |
. . . . . . . . . . . 12
⊢
(∃𝑢({𝑡} ∈ 𝑦 ∧ 𝑢 = {𝑡}) ↔ ({𝑡} ∈ 𝑦 ∧ ∃𝑢 𝑢 = {𝑡})) |
49 | 47, 48 | mpbiran2 708 |
. . . . . . . . . . 11
⊢
(∃𝑢({𝑡} ∈ 𝑦 ∧ 𝑢 = {𝑡}) ↔ {𝑡} ∈ 𝑦) |
50 | 45, 49 | bitri 274 |
. . . . . . . . . 10
⊢
(∃𝑢(𝑢 ∈ 𝑦 ∧ ∀𝑧 𝑢 = {𝑡}) ↔ {𝑡} ∈ 𝑦) |
51 | 34, 35, 50 | 3bitr4ri 303 |
. . . . . . . . 9
⊢
(∃𝑢(𝑢 ∈ 𝑦 ∧ ∀𝑧 𝑢 = {𝑡}) ↔ 𝑡 ∈ {𝑥 ∣ {𝑥} ∈ 𝑦}) |
52 | 51 | bibi2i 336 |
. . . . . . . 8
⊢ ((𝑡 ∈ 𝑧 ↔ ∃𝑢(𝑢 ∈ 𝑦 ∧ ∀𝑧 𝑢 = {𝑡})) ↔ (𝑡 ∈ 𝑧 ↔ 𝑡 ∈ {𝑥 ∣ {𝑥} ∈ 𝑦})) |
53 | 52 | albii 1814 |
. . . . . . 7
⊢
(∀𝑡(𝑡 ∈ 𝑧 ↔ ∃𝑢(𝑢 ∈ 𝑦 ∧ ∀𝑧 𝑢 = {𝑡})) ↔ ∀𝑡(𝑡 ∈ 𝑧 ↔ 𝑡 ∈ {𝑥 ∣ {𝑥} ∈ 𝑦})) |
54 | 53 | exbii 1843 |
. . . . . 6
⊢
(∃𝑧∀𝑡(𝑡 ∈ 𝑧 ↔ ∃𝑢(𝑢 ∈ 𝑦 ∧ ∀𝑧 𝑢 = {𝑡})) ↔ ∃𝑧∀𝑡(𝑡 ∈ 𝑧 ↔ 𝑡 ∈ {𝑥 ∣ {𝑥} ∈ 𝑦})) |
55 | 30, 54 | mpbi 229 |
. . . . 5
⊢
∃𝑧∀𝑡(𝑡 ∈ 𝑧 ↔ 𝑡 ∈ {𝑥 ∣ {𝑥} ∈ 𝑦}) |
56 | | dfcleq 2719 |
. . . . . 6
⊢ (𝑧 = {𝑥 ∣ {𝑥} ∈ 𝑦} ↔ ∀𝑡(𝑡 ∈ 𝑧 ↔ 𝑡 ∈ {𝑥 ∣ {𝑥} ∈ 𝑦})) |
57 | 56 | exbii 1843 |
. . . . 5
⊢
(∃𝑧 𝑧 = {𝑥 ∣ {𝑥} ∈ 𝑦} ↔ ∃𝑧∀𝑡(𝑡 ∈ 𝑧 ↔ 𝑡 ∈ {𝑥 ∣ {𝑥} ∈ 𝑦})) |
58 | 55, 57 | mpbir 230 |
. . . 4
⊢
∃𝑧 𝑧 = {𝑥 ∣ {𝑥} ∈ 𝑦} |
59 | 58 | issetri 3480 |
. . 3
⊢ {𝑥 ∣ {𝑥} ∈ 𝑦} ∈ V |
60 | 9, 59 | mpg 1792 |
. 2
⊢
(∃𝑦({𝑥 ∣ {𝑥} ∈ 𝑦} ∈ V → {𝑥 ∣ {𝑥} ∈ 𝐴} ∈ V) → ∃𝑦{𝑥 ∣ {𝑥} ∈ 𝐴} ∈ V) |
61 | | ax5e 1908 |
. 2
⊢
(∃𝑦{𝑥 ∣ {𝑥} ∈ 𝐴} ∈ V → {𝑥 ∣ {𝑥} ∈ 𝐴} ∈ V) |
62 | 1, 7, 60, 61 | 4syl 19 |
1
⊢ (𝐴 ∈ 𝑉 → {𝑥 ∣ {𝑥} ∈ 𝐴} ∈ V) |