Step | Hyp | Ref
| Expression |
1 | | eleq2 2677 |
. . . 4
⊢ (𝑧 = 𝐴 → (𝑥 ∈ 𝑧 ↔ 𝑥 ∈ 𝐴)) |
2 | 1 | exbidv 1837 |
. . 3
⊢ (𝑧 = 𝐴 → (∃𝑥 𝑥 ∈ 𝑧 ↔ ∃𝑥 𝑥 ∈ 𝐴)) |
3 | | eleq2 2677 |
. . . . . 6
⊢ (𝑧 = 𝐴 → (𝑦 ∈ 𝑧 ↔ 𝑦 ∈ 𝐴)) |
4 | 3 | notbid 307 |
. . . . 5
⊢ (𝑧 = 𝐴 → (¬ 𝑦 ∈ 𝑧 ↔ ¬ 𝑦 ∈ 𝐴)) |
5 | 4 | ralbidv 2969 |
. . . 4
⊢ (𝑧 = 𝐴 → (∀𝑦 ∈ 𝑥 ¬ 𝑦 ∈ 𝑧 ↔ ∀𝑦 ∈ 𝑥 ¬ 𝑦 ∈ 𝐴)) |
6 | 5 | rexeqbi1dv 3124 |
. . 3
⊢ (𝑧 = 𝐴 → (∃𝑥 ∈ 𝑧 ∀𝑦 ∈ 𝑥 ¬ 𝑦 ∈ 𝑧 ↔ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝑥 ¬ 𝑦 ∈ 𝐴)) |
7 | 2, 6 | imbi12d 333 |
. 2
⊢ (𝑧 = 𝐴 → ((∃𝑥 𝑥 ∈ 𝑧 → ∃𝑥 ∈ 𝑧 ∀𝑦 ∈ 𝑥 ¬ 𝑦 ∈ 𝑧) ↔ (∃𝑥 𝑥 ∈ 𝐴 → ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝑥 ¬ 𝑦 ∈ 𝐴))) |
8 | | nfre1 2988 |
. . 3
⊢
Ⅎ𝑥∃𝑥 ∈ 𝑧 ∀𝑦 ∈ 𝑥 ¬ 𝑦 ∈ 𝑧 |
9 | | axreg2 8381 |
. . . 4
⊢ (𝑥 ∈ 𝑧 → ∃𝑥(𝑥 ∈ 𝑧 ∧ ∀𝑦(𝑦 ∈ 𝑥 → ¬ 𝑦 ∈ 𝑧))) |
10 | | df-ral 2901 |
. . . . . 6
⊢
(∀𝑦 ∈
𝑥 ¬ 𝑦 ∈ 𝑧 ↔ ∀𝑦(𝑦 ∈ 𝑥 → ¬ 𝑦 ∈ 𝑧)) |
11 | 10 | rexbii 3023 |
. . . . 5
⊢
(∃𝑥 ∈
𝑧 ∀𝑦 ∈ 𝑥 ¬ 𝑦 ∈ 𝑧 ↔ ∃𝑥 ∈ 𝑧 ∀𝑦(𝑦 ∈ 𝑥 → ¬ 𝑦 ∈ 𝑧)) |
12 | | df-rex 2902 |
. . . . 5
⊢
(∃𝑥 ∈
𝑧 ∀𝑦(𝑦 ∈ 𝑥 → ¬ 𝑦 ∈ 𝑧) ↔ ∃𝑥(𝑥 ∈ 𝑧 ∧ ∀𝑦(𝑦 ∈ 𝑥 → ¬ 𝑦 ∈ 𝑧))) |
13 | 11, 12 | bitr2i 264 |
. . . 4
⊢
(∃𝑥(𝑥 ∈ 𝑧 ∧ ∀𝑦(𝑦 ∈ 𝑥 → ¬ 𝑦 ∈ 𝑧)) ↔ ∃𝑥 ∈ 𝑧 ∀𝑦 ∈ 𝑥 ¬ 𝑦 ∈ 𝑧) |
14 | 9, 13 | sylib 207 |
. . 3
⊢ (𝑥 ∈ 𝑧 → ∃𝑥 ∈ 𝑧 ∀𝑦 ∈ 𝑥 ¬ 𝑦 ∈ 𝑧) |
15 | 8, 14 | exlimi 2073 |
. 2
⊢
(∃𝑥 𝑥 ∈ 𝑧 → ∃𝑥 ∈ 𝑧 ∀𝑦 ∈ 𝑥 ¬ 𝑦 ∈ 𝑧) |
16 | 7, 15 | vtoclg 3239 |
1
⊢ (𝐴 ∈ 𝑉 → (∃𝑥 𝑥 ∈ 𝐴 → ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝑥 ¬ 𝑦 ∈ 𝐴)) |