Proof of Theorem dfnfc2
Step | Hyp | Ref
| Expression |
1 | | nfcvd 2300 |
. . . 4
⊢
(Ⅎ𝑥𝐴 → Ⅎ𝑥𝑦) |
2 | | id 19 |
. . . 4
⊢
(Ⅎ𝑥𝐴 → Ⅎ𝑥𝐴) |
3 | 1, 2 | nfeqd 2314 |
. . 3
⊢
(Ⅎ𝑥𝐴 → Ⅎ𝑥 𝑦 = 𝐴) |
4 | 3 | alrimiv 1854 |
. 2
⊢
(Ⅎ𝑥𝐴 → ∀𝑦Ⅎ𝑥 𝑦 = 𝐴) |
5 | | simpr 109 |
. . . . . 6
⊢
((∀𝑥 𝐴 ∈ 𝑉 ∧ ∀𝑦Ⅎ𝑥 𝑦 = 𝐴) → ∀𝑦Ⅎ𝑥 𝑦 = 𝐴) |
6 | | df-nfc 2288 |
. . . . . . 7
⊢
(Ⅎ𝑥{𝐴} ↔ ∀𝑦Ⅎ𝑥 𝑦 ∈ {𝐴}) |
7 | | velsn 3577 |
. . . . . . . . 9
⊢ (𝑦 ∈ {𝐴} ↔ 𝑦 = 𝐴) |
8 | 7 | nfbii 1453 |
. . . . . . . 8
⊢
(Ⅎ𝑥 𝑦 ∈ {𝐴} ↔ Ⅎ𝑥 𝑦 = 𝐴) |
9 | 8 | albii 1450 |
. . . . . . 7
⊢
(∀𝑦Ⅎ𝑥 𝑦 ∈ {𝐴} ↔ ∀𝑦Ⅎ𝑥 𝑦 = 𝐴) |
10 | 6, 9 | bitri 183 |
. . . . . 6
⊢
(Ⅎ𝑥{𝐴} ↔ ∀𝑦Ⅎ𝑥 𝑦 = 𝐴) |
11 | 5, 10 | sylibr 133 |
. . . . 5
⊢
((∀𝑥 𝐴 ∈ 𝑉 ∧ ∀𝑦Ⅎ𝑥 𝑦 = 𝐴) → Ⅎ𝑥{𝐴}) |
12 | 11 | nfunid 3779 |
. . . 4
⊢
((∀𝑥 𝐴 ∈ 𝑉 ∧ ∀𝑦Ⅎ𝑥 𝑦 = 𝐴) → Ⅎ𝑥∪ {𝐴}) |
13 | | nfa1 1521 |
. . . . . 6
⊢
Ⅎ𝑥∀𝑥 𝐴 ∈ 𝑉 |
14 | | nfnf1 1524 |
. . . . . . 7
⊢
Ⅎ𝑥Ⅎ𝑥 𝑦 = 𝐴 |
15 | 14 | nfal 1556 |
. . . . . 6
⊢
Ⅎ𝑥∀𝑦Ⅎ𝑥 𝑦 = 𝐴 |
16 | 13, 15 | nfan 1545 |
. . . . 5
⊢
Ⅎ𝑥(∀𝑥 𝐴 ∈ 𝑉 ∧ ∀𝑦Ⅎ𝑥 𝑦 = 𝐴) |
17 | | unisng 3789 |
. . . . . . 7
⊢ (𝐴 ∈ 𝑉 → ∪ {𝐴} = 𝐴) |
18 | 17 | sps 1517 |
. . . . . 6
⊢
(∀𝑥 𝐴 ∈ 𝑉 → ∪ {𝐴} = 𝐴) |
19 | 18 | adantr 274 |
. . . . 5
⊢
((∀𝑥 𝐴 ∈ 𝑉 ∧ ∀𝑦Ⅎ𝑥 𝑦 = 𝐴) → ∪ {𝐴} = 𝐴) |
20 | 16, 19 | nfceqdf 2298 |
. . . 4
⊢
((∀𝑥 𝐴 ∈ 𝑉 ∧ ∀𝑦Ⅎ𝑥 𝑦 = 𝐴) → (Ⅎ𝑥∪ {𝐴} ↔ Ⅎ𝑥𝐴)) |
21 | 12, 20 | mpbid 146 |
. . 3
⊢
((∀𝑥 𝐴 ∈ 𝑉 ∧ ∀𝑦Ⅎ𝑥 𝑦 = 𝐴) → Ⅎ𝑥𝐴) |
22 | 21 | ex 114 |
. 2
⊢
(∀𝑥 𝐴 ∈ 𝑉 → (∀𝑦Ⅎ𝑥 𝑦 = 𝐴 → Ⅎ𝑥𝐴)) |
23 | 4, 22 | impbid2 142 |
1
⊢
(∀𝑥 𝐴 ∈ 𝑉 → (Ⅎ𝑥𝐴 ↔ ∀𝑦Ⅎ𝑥 𝑦 = 𝐴)) |