Proof of Theorem dfnfc2OLD
Step | Hyp | Ref
| Expression |
1 | | nfcvd 2752 |
. . . 4
⊢
(Ⅎ𝑥𝐴 → Ⅎ𝑥𝑦) |
2 | | id 22 |
. . . 4
⊢
(Ⅎ𝑥𝐴 → Ⅎ𝑥𝐴) |
3 | 1, 2 | nfeqd 2758 |
. . 3
⊢
(Ⅎ𝑥𝐴 → Ⅎ𝑥 𝑦 = 𝐴) |
4 | 3 | alrimiv 1842 |
. 2
⊢
(Ⅎ𝑥𝐴 → ∀𝑦Ⅎ𝑥 𝑦 = 𝐴) |
5 | | simpr 476 |
. . . . . 6
⊢
((∀𝑥 𝐴 ∈ 𝑉 ∧ ∀𝑦Ⅎ𝑥 𝑦 = 𝐴) → ∀𝑦Ⅎ𝑥 𝑦 = 𝐴) |
6 | | df-nfc 2740 |
. . . . . . 7
⊢
(Ⅎ𝑥{𝐴} ↔ ∀𝑦Ⅎ𝑥 𝑦 ∈ {𝐴}) |
7 | | velsn 4141 |
. . . . . . . . 9
⊢ (𝑦 ∈ {𝐴} ↔ 𝑦 = 𝐴) |
8 | 7 | nfbii 1770 |
. . . . . . . 8
⊢
(Ⅎ𝑥 𝑦 ∈ {𝐴} ↔ Ⅎ𝑥 𝑦 = 𝐴) |
9 | 8 | albii 1737 |
. . . . . . 7
⊢
(∀𝑦Ⅎ𝑥 𝑦 ∈ {𝐴} ↔ ∀𝑦Ⅎ𝑥 𝑦 = 𝐴) |
10 | 6, 9 | bitri 263 |
. . . . . 6
⊢
(Ⅎ𝑥{𝐴} ↔ ∀𝑦Ⅎ𝑥 𝑦 = 𝐴) |
11 | 5, 10 | sylibr 223 |
. . . . 5
⊢
((∀𝑥 𝐴 ∈ 𝑉 ∧ ∀𝑦Ⅎ𝑥 𝑦 = 𝐴) → Ⅎ𝑥{𝐴}) |
12 | 11 | nfunid 4379 |
. . . 4
⊢
((∀𝑥 𝐴 ∈ 𝑉 ∧ ∀𝑦Ⅎ𝑥 𝑦 = 𝐴) → Ⅎ𝑥∪ {𝐴}) |
13 | | nfa1 2015 |
. . . . . 6
⊢
Ⅎ𝑥∀𝑥 𝐴 ∈ 𝑉 |
14 | | nfnf1 2018 |
. . . . . . 7
⊢
Ⅎ𝑥Ⅎ𝑥 𝑦 = 𝐴 |
15 | 14 | nfal 2139 |
. . . . . 6
⊢
Ⅎ𝑥∀𝑦Ⅎ𝑥 𝑦 = 𝐴 |
16 | 13, 15 | nfan 1816 |
. . . . 5
⊢
Ⅎ𝑥(∀𝑥 𝐴 ∈ 𝑉 ∧ ∀𝑦Ⅎ𝑥 𝑦 = 𝐴) |
17 | | unisng 4388 |
. . . . . . 7
⊢ (𝐴 ∈ 𝑉 → ∪ {𝐴} = 𝐴) |
18 | 17 | sps 2043 |
. . . . . 6
⊢
(∀𝑥 𝐴 ∈ 𝑉 → ∪ {𝐴} = 𝐴) |
19 | 18 | adantr 480 |
. . . . 5
⊢
((∀𝑥 𝐴 ∈ 𝑉 ∧ ∀𝑦Ⅎ𝑥 𝑦 = 𝐴) → ∪ {𝐴} = 𝐴) |
20 | 16, 19 | nfceqdf 2747 |
. . . 4
⊢
((∀𝑥 𝐴 ∈ 𝑉 ∧ ∀𝑦Ⅎ𝑥 𝑦 = 𝐴) → (Ⅎ𝑥∪ {𝐴} ↔ Ⅎ𝑥𝐴)) |
21 | 12, 20 | mpbid 221 |
. . 3
⊢
((∀𝑥 𝐴 ∈ 𝑉 ∧ ∀𝑦Ⅎ𝑥 𝑦 = 𝐴) → Ⅎ𝑥𝐴) |
22 | 21 | ex 449 |
. 2
⊢
(∀𝑥 𝐴 ∈ 𝑉 → (∀𝑦Ⅎ𝑥 𝑦 = 𝐴 → Ⅎ𝑥𝐴)) |
23 | 4, 22 | impbid2 215 |
1
⊢
(∀𝑥 𝐴 ∈ 𝑉 → (Ⅎ𝑥𝐴 ↔ ∀𝑦Ⅎ𝑥 𝑦 = 𝐴)) |