Step | Hyp | Ref
| Expression |
1 | | eliin 4461 |
. . 3
⊢ (𝐴 ∈ V → (𝐴 ∈ ∩ 𝑥 ∈ 𝐵 𝐶 ↔ ∀𝑥 ∈ 𝐵 𝐴 ∈ 𝐶)) |
2 | 1 | adantl 481 |
. 2
⊢ ((𝐵 ≠ ∅ ∧ 𝐴 ∈ V) → (𝐴 ∈ ∩ 𝑥 ∈ 𝐵 𝐶 ↔ ∀𝑥 ∈ 𝐵 𝐴 ∈ 𝐶)) |
3 | | prcnel 3191 |
. . . . 5
⊢ (¬
𝐴 ∈ V → ¬
𝐴 ∈ ∩ 𝑥 ∈ 𝐵 𝐶) |
4 | 3 | adantl 481 |
. . . 4
⊢ ((𝐵 ≠ ∅ ∧ ¬ 𝐴 ∈ V) → ¬ 𝐴 ∈ ∩ 𝑥 ∈ 𝐵 𝐶) |
5 | | n0 3890 |
. . . . . . . . . 10
⊢ (𝐵 ≠ ∅ ↔
∃𝑦 𝑦 ∈ 𝐵) |
6 | 5 | biimpi 205 |
. . . . . . . . 9
⊢ (𝐵 ≠ ∅ →
∃𝑦 𝑦 ∈ 𝐵) |
7 | 6 | adantr 480 |
. . . . . . . 8
⊢ ((𝐵 ≠ ∅ ∧ ¬ 𝐴 ∈ V) → ∃𝑦 𝑦 ∈ 𝐵) |
8 | | prcnel 3191 |
. . . . . . . . . . . 12
⊢ (¬
𝐴 ∈ V → ¬
𝐴 ∈
⦋𝑦 / 𝑥⦌𝐶) |
9 | 8 | a1d 25 |
. . . . . . . . . . 11
⊢ (¬
𝐴 ∈ V → (𝑦 ∈ 𝐵 → ¬ 𝐴 ∈ ⦋𝑦 / 𝑥⦌𝐶)) |
10 | 9 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝐵 ≠ ∅ ∧ ¬ 𝐴 ∈ V) → (𝑦 ∈ 𝐵 → ¬ 𝐴 ∈ ⦋𝑦 / 𝑥⦌𝐶)) |
11 | 10 | ancld 574 |
. . . . . . . . 9
⊢ ((𝐵 ≠ ∅ ∧ ¬ 𝐴 ∈ V) → (𝑦 ∈ 𝐵 → (𝑦 ∈ 𝐵 ∧ ¬ 𝐴 ∈ ⦋𝑦 / 𝑥⦌𝐶))) |
12 | 11 | eximdv 1833 |
. . . . . . . 8
⊢ ((𝐵 ≠ ∅ ∧ ¬ 𝐴 ∈ V) → (∃𝑦 𝑦 ∈ 𝐵 → ∃𝑦(𝑦 ∈ 𝐵 ∧ ¬ 𝐴 ∈ ⦋𝑦 / 𝑥⦌𝐶))) |
13 | 7, 12 | mpd 15 |
. . . . . . 7
⊢ ((𝐵 ≠ ∅ ∧ ¬ 𝐴 ∈ V) → ∃𝑦(𝑦 ∈ 𝐵 ∧ ¬ 𝐴 ∈ ⦋𝑦 / 𝑥⦌𝐶)) |
14 | | df-rex 2902 |
. . . . . . 7
⊢
(∃𝑦 ∈
𝐵 ¬ 𝐴 ∈ ⦋𝑦 / 𝑥⦌𝐶 ↔ ∃𝑦(𝑦 ∈ 𝐵 ∧ ¬ 𝐴 ∈ ⦋𝑦 / 𝑥⦌𝐶)) |
15 | 13, 14 | sylibr 223 |
. . . . . 6
⊢ ((𝐵 ≠ ∅ ∧ ¬ 𝐴 ∈ V) → ∃𝑦 ∈ 𝐵 ¬ 𝐴 ∈ ⦋𝑦 / 𝑥⦌𝐶) |
16 | | eliin2f.1 |
. . . . . . 7
⊢
Ⅎ𝑥𝐵 |
17 | | nfcv 2751 |
. . . . . . 7
⊢
Ⅎ𝑦𝐵 |
18 | | nfv 1830 |
. . . . . . 7
⊢
Ⅎ𝑦 ¬ 𝐴 ∈ 𝐶 |
19 | | nfcv 2751 |
. . . . . . . . 9
⊢
Ⅎ𝑥𝐴 |
20 | | nfcsb1v 3515 |
. . . . . . . . 9
⊢
Ⅎ𝑥⦋𝑦 / 𝑥⦌𝐶 |
21 | 19, 20 | nfel 2763 |
. . . . . . . 8
⊢
Ⅎ𝑥 𝐴 ∈ ⦋𝑦 / 𝑥⦌𝐶 |
22 | 21 | nfn 1768 |
. . . . . . 7
⊢
Ⅎ𝑥 ¬ 𝐴 ∈ ⦋𝑦 / 𝑥⦌𝐶 |
23 | | csbeq1a 3508 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → 𝐶 = ⦋𝑦 / 𝑥⦌𝐶) |
24 | 23 | eleq2d 2673 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → (𝐴 ∈ 𝐶 ↔ 𝐴 ∈ ⦋𝑦 / 𝑥⦌𝐶)) |
25 | 24 | notbid 307 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → (¬ 𝐴 ∈ 𝐶 ↔ ¬ 𝐴 ∈ ⦋𝑦 / 𝑥⦌𝐶)) |
26 | 16, 17, 18, 22, 25 | cbvrexf 3142 |
. . . . . 6
⊢
(∃𝑥 ∈
𝐵 ¬ 𝐴 ∈ 𝐶 ↔ ∃𝑦 ∈ 𝐵 ¬ 𝐴 ∈ ⦋𝑦 / 𝑥⦌𝐶) |
27 | 15, 26 | sylibr 223 |
. . . . 5
⊢ ((𝐵 ≠ ∅ ∧ ¬ 𝐴 ∈ V) → ∃𝑥 ∈ 𝐵 ¬ 𝐴 ∈ 𝐶) |
28 | | rexnal 2978 |
. . . . 5
⊢
(∃𝑥 ∈
𝐵 ¬ 𝐴 ∈ 𝐶 ↔ ¬ ∀𝑥 ∈ 𝐵 𝐴 ∈ 𝐶) |
29 | 27, 28 | sylib 207 |
. . . 4
⊢ ((𝐵 ≠ ∅ ∧ ¬ 𝐴 ∈ V) → ¬
∀𝑥 ∈ 𝐵 𝐴 ∈ 𝐶) |
30 | 4, 29 | jca 553 |
. . 3
⊢ ((𝐵 ≠ ∅ ∧ ¬ 𝐴 ∈ V) → (¬ 𝐴 ∈ ∩ 𝑥 ∈ 𝐵 𝐶 ∧ ¬ ∀𝑥 ∈ 𝐵 𝐴 ∈ 𝐶)) |
31 | | pm5.21 899 |
. . 3
⊢ ((¬
𝐴 ∈ ∩ 𝑥 ∈ 𝐵 𝐶 ∧ ¬ ∀𝑥 ∈ 𝐵 𝐴 ∈ 𝐶) → (𝐴 ∈ ∩
𝑥 ∈ 𝐵 𝐶 ↔ ∀𝑥 ∈ 𝐵 𝐴 ∈ 𝐶)) |
32 | 30, 31 | syl 17 |
. 2
⊢ ((𝐵 ≠ ∅ ∧ ¬ 𝐴 ∈ V) → (𝐴 ∈ ∩ 𝑥 ∈ 𝐵 𝐶 ↔ ∀𝑥 ∈ 𝐵 𝐴 ∈ 𝐶)) |
33 | 2, 32 | pm2.61dan 828 |
1
⊢ (𝐵 ≠ ∅ → (𝐴 ∈ ∩ 𝑥 ∈ 𝐵 𝐶 ↔ ∀𝑥 ∈ 𝐵 𝐴 ∈ 𝐶)) |