Step | Hyp | Ref
| Expression |
1 | | elisset 3426 |
. . . 4
⊢ (𝐴 ∈ 𝑉 → ∃𝑦 𝑦 = 𝐴) |
2 | | eleq2 2854 |
. . . . . . 7
⊢ (𝑦 = 𝐴 → ({𝑥} ∈ 𝑦 ↔ {𝑥} ∈ 𝐴)) |
3 | 2 | abbidv 2843 |
. . . . . 6
⊢ (𝑦 = 𝐴 → {𝑥 ∣ {𝑥} ∈ 𝑦} = {𝑥 ∣ {𝑥} ∈ 𝐴}) |
4 | | eleq1 2853 |
. . . . . . 7
⊢ ({𝑥 ∣ {𝑥} ∈ 𝑦} = {𝑥 ∣ {𝑥} ∈ 𝐴} → ({𝑥 ∣ {𝑥} ∈ 𝑦} ∈ V ↔ {𝑥 ∣ {𝑥} ∈ 𝐴} ∈ V)) |
5 | 4 | biimpd 221 |
. . . . . 6
⊢ ({𝑥 ∣ {𝑥} ∈ 𝑦} = {𝑥 ∣ {𝑥} ∈ 𝐴} → ({𝑥 ∣ {𝑥} ∈ 𝑦} ∈ V → {𝑥 ∣ {𝑥} ∈ 𝐴} ∈ V)) |
6 | 3, 5 | syl 17 |
. . . . 5
⊢ (𝑦 = 𝐴 → ({𝑥 ∣ {𝑥} ∈ 𝑦} ∈ V → {𝑥 ∣ {𝑥} ∈ 𝐴} ∈ V)) |
7 | 6 | eximi 1797 |
. . . 4
⊢
(∃𝑦 𝑦 = 𝐴 → ∃𝑦({𝑥 ∣ {𝑥} ∈ 𝑦} ∈ V → {𝑥 ∣ {𝑥} ∈ 𝐴} ∈ V)) |
8 | 1, 7 | syl 17 |
. . 3
⊢ (𝐴 ∈ 𝑉 → ∃𝑦({𝑥 ∣ {𝑥} ∈ 𝑦} ∈ V → {𝑥 ∣ {𝑥} ∈ 𝐴} ∈ V)) |
9 | | 19.35 1840 |
. . . . . 6
⊢
(∃𝑦({𝑥 ∣ {𝑥} ∈ 𝑦} ∈ V → {𝑥 ∣ {𝑥} ∈ 𝐴} ∈ V) ↔ (∀𝑦{𝑥 ∣ {𝑥} ∈ 𝑦} ∈ V → ∃𝑦{𝑥 ∣ {𝑥} ∈ 𝐴} ∈ V)) |
10 | 9 | biimpi 208 |
. . . . 5
⊢
(∃𝑦({𝑥 ∣ {𝑥} ∈ 𝑦} ∈ V → {𝑥 ∣ {𝑥} ∈ 𝐴} ∈ V) → (∀𝑦{𝑥 ∣ {𝑥} ∈ 𝑦} ∈ V → ∃𝑦{𝑥 ∣ {𝑥} ∈ 𝐴} ∈ V)) |
11 | 10 | com12 32 |
. . . 4
⊢
(∀𝑦{𝑥 ∣ {𝑥} ∈ 𝑦} ∈ V → (∃𝑦({𝑥 ∣ {𝑥} ∈ 𝑦} ∈ V → {𝑥 ∣ {𝑥} ∈ 𝐴} ∈ V) → ∃𝑦{𝑥 ∣ {𝑥} ∈ 𝐴} ∈ V)) |
12 | | ax-rep 5049 |
. . . . . . . 8
⊢
(∀𝑢∃𝑧∀𝑡(∀𝑧 𝑢 = {𝑡} → 𝑡 = 𝑧) → ∃𝑧∀𝑡(𝑡 ∈ 𝑧 ↔ ∃𝑢(𝑢 ∈ 𝑦 ∧ ∀𝑧 𝑢 = {𝑡}))) |
13 | | 19.3v 1939 |
. . . . . . . . . . 11
⊢
(∀𝑧 𝑢 = {𝑡} ↔ 𝑢 = {𝑡}) |
14 | 13 | sbbii 2027 |
. . . . . . . . . . 11
⊢ ([𝑧 / 𝑡]∀𝑧 𝑢 = {𝑡} ↔ [𝑧 / 𝑡]𝑢 = {𝑡}) |
15 | | sbsbc 3685 |
. . . . . . . . . . . . . 14
⊢ ([𝑧 / 𝑡]𝑢 = {𝑡} ↔ [𝑧 / 𝑡]𝑢 = {𝑡}) |
16 | | sbceq2g 4254 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 ∈ V → ([𝑧 / 𝑡]𝑢 = {𝑡} ↔ 𝑢 = ⦋𝑧 / 𝑡⦌{𝑡})) |
17 | 16 | elv 3420 |
. . . . . . . . . . . . . 14
⊢
([𝑧 / 𝑡]𝑢 = {𝑡} ↔ 𝑢 = ⦋𝑧 / 𝑡⦌{𝑡}) |
18 | 15, 17 | bitri 267 |
. . . . . . . . . . . . 13
⊢ ([𝑧 / 𝑡]𝑢 = {𝑡} ↔ 𝑢 = ⦋𝑧 / 𝑡⦌{𝑡}) |
19 | | bj-csbsn 33719 |
. . . . . . . . . . . . . 14
⊢
⦋𝑧 /
𝑡⦌{𝑡} = {𝑧} |
20 | 19 | eqeq2i 2790 |
. . . . . . . . . . . . 13
⊢ (𝑢 = ⦋𝑧 / 𝑡⦌{𝑡} ↔ 𝑢 = {𝑧}) |
21 | 18, 20 | bitri 267 |
. . . . . . . . . . . 12
⊢ ([𝑧 / 𝑡]𝑢 = {𝑡} ↔ 𝑢 = {𝑧}) |
22 | | eqtr2 2800 |
. . . . . . . . . . . . 13
⊢ ((𝑢 = {𝑡} ∧ 𝑢 = {𝑧}) → {𝑡} = {𝑧}) |
23 | | vex 3418 |
. . . . . . . . . . . . . 14
⊢ 𝑡 ∈ V |
24 | 23 | sneqr 4645 |
. . . . . . . . . . . . 13
⊢ ({𝑡} = {𝑧} → 𝑡 = 𝑧) |
25 | 22, 24 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝑢 = {𝑡} ∧ 𝑢 = {𝑧}) → 𝑡 = 𝑧) |
26 | 21, 25 | sylan2b 584 |
. . . . . . . . . . 11
⊢ ((𝑢 = {𝑡} ∧ [𝑧 / 𝑡]𝑢 = {𝑡}) → 𝑡 = 𝑧) |
27 | 13, 14, 26 | syl2anb 588 |
. . . . . . . . . 10
⊢
((∀𝑧 𝑢 = {𝑡} ∧ [𝑧 / 𝑡]∀𝑧 𝑢 = {𝑡}) → 𝑡 = 𝑧) |
28 | 27 | gen2 1759 |
. . . . . . . . 9
⊢
∀𝑡∀𝑧((∀𝑧 𝑢 = {𝑡} ∧ [𝑧 / 𝑡]∀𝑧 𝑢 = {𝑡}) → 𝑡 = 𝑧) |
29 | | nfa1 2088 |
. . . . . . . . . 10
⊢
Ⅎ𝑧∀𝑧 𝑢 = {𝑡} |
30 | 29 | mo 2579 |
. . . . . . . . 9
⊢
(∃𝑧∀𝑡(∀𝑧 𝑢 = {𝑡} → 𝑡 = 𝑧) ↔ ∀𝑡∀𝑧((∀𝑧 𝑢 = {𝑡} ∧ [𝑧 / 𝑡]∀𝑧 𝑢 = {𝑡}) → 𝑡 = 𝑧)) |
31 | 28, 30 | mpbir 223 |
. . . . . . . 8
⊢
∃𝑧∀𝑡(∀𝑧 𝑢 = {𝑡} → 𝑡 = 𝑧) |
32 | 12, 31 | mpg 1760 |
. . . . . . 7
⊢
∃𝑧∀𝑡(𝑡 ∈ 𝑧 ↔ ∃𝑢(𝑢 ∈ 𝑦 ∧ ∀𝑧 𝑢 = {𝑡})) |
33 | | bj-sbel1 33720 |
. . . . . . . . . . . 12
⊢ ([𝑡 / 𝑥]{𝑥} ∈ 𝑦 ↔ ⦋𝑡 / 𝑥⦌{𝑥} ∈ 𝑦) |
34 | | bj-csbsn 33719 |
. . . . . . . . . . . . 13
⊢
⦋𝑡 /
𝑥⦌{𝑥} = {𝑡} |
35 | 34 | eleq1i 2856 |
. . . . . . . . . . . 12
⊢
(⦋𝑡 /
𝑥⦌{𝑥} ∈ 𝑦 ↔ {𝑡} ∈ 𝑦) |
36 | 33, 35 | bitri 267 |
. . . . . . . . . . 11
⊢ ([𝑡 / 𝑥]{𝑥} ∈ 𝑦 ↔ {𝑡} ∈ 𝑦) |
37 | | df-clab 2759 |
. . . . . . . . . . 11
⊢ (𝑡 ∈ {𝑥 ∣ {𝑥} ∈ 𝑦} ↔ [𝑡 / 𝑥]{𝑥} ∈ 𝑦) |
38 | 13 | anbi2i 613 |
. . . . . . . . . . . . . 14
⊢ ((𝑢 ∈ 𝑦 ∧ ∀𝑧 𝑢 = {𝑡}) ↔ (𝑢 ∈ 𝑦 ∧ 𝑢 = {𝑡})) |
39 | | eleq1a 2861 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑢 ∈ 𝑦 → ({𝑡} = 𝑢 → {𝑡} ∈ 𝑦)) |
40 | 39 | com12 32 |
. . . . . . . . . . . . . . . . 17
⊢ ({𝑡} = 𝑢 → (𝑢 ∈ 𝑦 → {𝑡} ∈ 𝑦)) |
41 | 40 | eqcoms 2786 |
. . . . . . . . . . . . . . . 16
⊢ (𝑢 = {𝑡} → (𝑢 ∈ 𝑦 → {𝑡} ∈ 𝑦)) |
42 | 41 | imdistanri 562 |
. . . . . . . . . . . . . . 15
⊢ ((𝑢 ∈ 𝑦 ∧ 𝑢 = {𝑡}) → ({𝑡} ∈ 𝑦 ∧ 𝑢 = {𝑡})) |
43 | | eleq1a 2861 |
. . . . . . . . . . . . . . . 16
⊢ ({𝑡} ∈ 𝑦 → (𝑢 = {𝑡} → 𝑢 ∈ 𝑦)) |
44 | 43 | impac 545 |
. . . . . . . . . . . . . . 15
⊢ (({𝑡} ∈ 𝑦 ∧ 𝑢 = {𝑡}) → (𝑢 ∈ 𝑦 ∧ 𝑢 = {𝑡})) |
45 | 42, 44 | impbii 201 |
. . . . . . . . . . . . . 14
⊢ ((𝑢 ∈ 𝑦 ∧ 𝑢 = {𝑡}) ↔ ({𝑡} ∈ 𝑦 ∧ 𝑢 = {𝑡})) |
46 | 38, 45 | bitri 267 |
. . . . . . . . . . . . 13
⊢ ((𝑢 ∈ 𝑦 ∧ ∀𝑧 𝑢 = {𝑡}) ↔ ({𝑡} ∈ 𝑦 ∧ 𝑢 = {𝑡})) |
47 | 46 | exbii 1810 |
. . . . . . . . . . . 12
⊢
(∃𝑢(𝑢 ∈ 𝑦 ∧ ∀𝑧 𝑢 = {𝑡}) ↔ ∃𝑢({𝑡} ∈ 𝑦 ∧ 𝑢 = {𝑡})) |
48 | | snex 5188 |
. . . . . . . . . . . . . 14
⊢ {𝑡} ∈ V |
49 | 48 | isseti 3429 |
. . . . . . . . . . . . 13
⊢
∃𝑢 𝑢 = {𝑡} |
50 | | 19.42v 1912 |
. . . . . . . . . . . . 13
⊢
(∃𝑢({𝑡} ∈ 𝑦 ∧ 𝑢 = {𝑡}) ↔ ({𝑡} ∈ 𝑦 ∧ ∃𝑢 𝑢 = {𝑡})) |
51 | 49, 50 | mpbiran2 697 |
. . . . . . . . . . . 12
⊢
(∃𝑢({𝑡} ∈ 𝑦 ∧ 𝑢 = {𝑡}) ↔ {𝑡} ∈ 𝑦) |
52 | 47, 51 | bitri 267 |
. . . . . . . . . . 11
⊢
(∃𝑢(𝑢 ∈ 𝑦 ∧ ∀𝑧 𝑢 = {𝑡}) ↔ {𝑡} ∈ 𝑦) |
53 | 36, 37, 52 | 3bitr4ri 296 |
. . . . . . . . . 10
⊢
(∃𝑢(𝑢 ∈ 𝑦 ∧ ∀𝑧 𝑢 = {𝑡}) ↔ 𝑡 ∈ {𝑥 ∣ {𝑥} ∈ 𝑦}) |
54 | 53 | bibi2i 330 |
. . . . . . . . 9
⊢ ((𝑡 ∈ 𝑧 ↔ ∃𝑢(𝑢 ∈ 𝑦 ∧ ∀𝑧 𝑢 = {𝑡})) ↔ (𝑡 ∈ 𝑧 ↔ 𝑡 ∈ {𝑥 ∣ {𝑥} ∈ 𝑦})) |
55 | 54 | albii 1782 |
. . . . . . . 8
⊢
(∀𝑡(𝑡 ∈ 𝑧 ↔ ∃𝑢(𝑢 ∈ 𝑦 ∧ ∀𝑧 𝑢 = {𝑡})) ↔ ∀𝑡(𝑡 ∈ 𝑧 ↔ 𝑡 ∈ {𝑥 ∣ {𝑥} ∈ 𝑦})) |
56 | 55 | exbii 1810 |
. . . . . . 7
⊢
(∃𝑧∀𝑡(𝑡 ∈ 𝑧 ↔ ∃𝑢(𝑢 ∈ 𝑦 ∧ ∀𝑧 𝑢 = {𝑡})) ↔ ∃𝑧∀𝑡(𝑡 ∈ 𝑧 ↔ 𝑡 ∈ {𝑥 ∣ {𝑥} ∈ 𝑦})) |
57 | 32, 56 | mpbi 222 |
. . . . . 6
⊢
∃𝑧∀𝑡(𝑡 ∈ 𝑧 ↔ 𝑡 ∈ {𝑥 ∣ {𝑥} ∈ 𝑦}) |
58 | | dfcleq 2772 |
. . . . . . 7
⊢ (𝑧 = {𝑥 ∣ {𝑥} ∈ 𝑦} ↔ ∀𝑡(𝑡 ∈ 𝑧 ↔ 𝑡 ∈ {𝑥 ∣ {𝑥} ∈ 𝑦})) |
59 | 58 | exbii 1810 |
. . . . . 6
⊢
(∃𝑧 𝑧 = {𝑥 ∣ {𝑥} ∈ 𝑦} ↔ ∃𝑧∀𝑡(𝑡 ∈ 𝑧 ↔ 𝑡 ∈ {𝑥 ∣ {𝑥} ∈ 𝑦})) |
60 | 57, 59 | mpbir 223 |
. . . . 5
⊢
∃𝑧 𝑧 = {𝑥 ∣ {𝑥} ∈ 𝑦} |
61 | 60 | issetri 3431 |
. . . 4
⊢ {𝑥 ∣ {𝑥} ∈ 𝑦} ∈ V |
62 | 11, 61 | mpg 1760 |
. . 3
⊢
(∃𝑦({𝑥 ∣ {𝑥} ∈ 𝑦} ∈ V → {𝑥 ∣ {𝑥} ∈ 𝐴} ∈ V) → ∃𝑦{𝑥 ∣ {𝑥} ∈ 𝐴} ∈ V) |
63 | 8, 62 | syl 17 |
. 2
⊢ (𝐴 ∈ 𝑉 → ∃𝑦{𝑥 ∣ {𝑥} ∈ 𝐴} ∈ V) |
64 | | ax5e 1871 |
. 2
⊢
(∃𝑦{𝑥 ∣ {𝑥} ∈ 𝐴} ∈ V → {𝑥 ∣ {𝑥} ∈ 𝐴} ∈ V) |
65 | 63, 64 | syl 17 |
1
⊢ (𝐴 ∈ 𝑉 → {𝑥 ∣ {𝑥} ∈ 𝐴} ∈ V) |