Step | Hyp | Ref
| Expression |
1 | | simpl1 1190 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ≠ 𝐵) ∧ (𝜓 ∧ 𝜒)) → 𝐴 ∈ 𝑋) |
2 | | simpl2 1191 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ≠ 𝐵) ∧ (𝜓 ∧ 𝜒)) → 𝐵 ∈ 𝑋) |
3 | | simprl 768 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ≠ 𝐵) ∧ (𝜓 ∧ 𝜒)) → 𝜓) |
4 | | 2nreu.b |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜒)) |
5 | 4 | sbcieg 3756 |
. . . . . . . . . . 11
⊢ (𝐵 ∈ 𝑋 → ([𝐵 / 𝑥]𝜑 ↔ 𝜒)) |
6 | 5 | 3ad2ant2 1133 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ≠ 𝐵) → ([𝐵 / 𝑥]𝜑 ↔ 𝜒)) |
7 | 6 | biimprd 247 |
. . . . . . . . 9
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ≠ 𝐵) → (𝜒 → [𝐵 / 𝑥]𝜑)) |
8 | 7 | adantld 491 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ≠ 𝐵) → ((𝜓 ∧ 𝜒) → [𝐵 / 𝑥]𝜑)) |
9 | 8 | imp 407 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ≠ 𝐵) ∧ (𝜓 ∧ 𝜒)) → [𝐵 / 𝑥]𝜑) |
10 | 3, 9 | jca 512 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ≠ 𝐵) ∧ (𝜓 ∧ 𝜒)) → (𝜓 ∧ [𝐵 / 𝑥]𝜑)) |
11 | | simpl3 1192 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ≠ 𝐵) ∧ (𝜓 ∧ 𝜒)) → 𝐴 ≠ 𝐵) |
12 | | simp1 1135 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ((𝜓 ∧ [𝐵 / 𝑥]𝜑) ∧ 𝐴 ≠ 𝐵)) → 𝐴 ∈ 𝑋) |
13 | | simp2 1136 |
. . . . . . . . 9
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ((𝜓 ∧ [𝐵 / 𝑥]𝜑) ∧ 𝐴 ≠ 𝐵)) → 𝐵 ∈ 𝑋) |
14 | | simp3 1137 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ((𝜓 ∧ [𝐵 / 𝑥]𝜑) ∧ 𝐴 ≠ 𝐵)) → ((𝜓 ∧ [𝐵 / 𝑥]𝜑) ∧ 𝐴 ≠ 𝐵)) |
15 | | sbcan 3768 |
. . . . . . . . . . . . . 14
⊢
([𝐴 / 𝑥]((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝑥 ≠ 𝑦) ↔ ([𝐴 / 𝑥](𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ [𝐴 / 𝑥]𝑥 ≠ 𝑦)) |
16 | | sbcan 3768 |
. . . . . . . . . . . . . . . 16
⊢
([𝐴 / 𝑥](𝜑 ∧ [𝑦 / 𝑥]𝜑) ↔ ([𝐴 / 𝑥]𝜑 ∧ [𝐴 / 𝑥][𝑦 / 𝑥]𝜑)) |
17 | | 2nreu.a |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) |
18 | 17 | sbcieg 3756 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴 ∈ 𝑋 → ([𝐴 / 𝑥]𝜑 ↔ 𝜓)) |
19 | | nfs1v 2153 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑥[𝑦 / 𝑥]𝜑 |
20 | 19 | sbcgf 3793 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴 ∈ 𝑋 → ([𝐴 / 𝑥][𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑)) |
21 | 18, 20 | anbi12d 631 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ 𝑋 → (([𝐴 / 𝑥]𝜑 ∧ [𝐴 / 𝑥][𝑦 / 𝑥]𝜑) ↔ (𝜓 ∧ [𝑦 / 𝑥]𝜑))) |
22 | 16, 21 | bitrid 282 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ 𝑋 → ([𝐴 / 𝑥](𝜑 ∧ [𝑦 / 𝑥]𝜑) ↔ (𝜓 ∧ [𝑦 / 𝑥]𝜑))) |
23 | | sbcne12 4346 |
. . . . . . . . . . . . . . . 16
⊢
([𝐴 / 𝑥]𝑥 ≠ 𝑦 ↔ ⦋𝐴 / 𝑥⦌𝑥 ≠ ⦋𝐴 / 𝑥⦌𝑦) |
24 | | csbvarg 4365 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴 ∈ 𝑋 → ⦋𝐴 / 𝑥⦌𝑥 = 𝐴) |
25 | | csbconstg 3851 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴 ∈ 𝑋 → ⦋𝐴 / 𝑥⦌𝑦 = 𝑦) |
26 | 24, 25 | neeq12d 3005 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ 𝑋 → (⦋𝐴 / 𝑥⦌𝑥 ≠ ⦋𝐴 / 𝑥⦌𝑦 ↔ 𝐴 ≠ 𝑦)) |
27 | 23, 26 | bitrid 282 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ 𝑋 → ([𝐴 / 𝑥]𝑥 ≠ 𝑦 ↔ 𝐴 ≠ 𝑦)) |
28 | 22, 27 | anbi12d 631 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ 𝑋 → (([𝐴 / 𝑥](𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ [𝐴 / 𝑥]𝑥 ≠ 𝑦) ↔ ((𝜓 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝐴 ≠ 𝑦))) |
29 | 15, 28 | bitrid 282 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ 𝑋 → ([𝐴 / 𝑥]((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝑥 ≠ 𝑦) ↔ ((𝜓 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝐴 ≠ 𝑦))) |
30 | 29 | 3ad2ant1 1132 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ((𝜓 ∧ [𝐵 / 𝑥]𝜑) ∧ 𝐴 ≠ 𝐵)) → ([𝐴 / 𝑥]((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝑥 ≠ 𝑦) ↔ ((𝜓 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝐴 ≠ 𝑦))) |
31 | 30 | sbcbidv 3775 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ((𝜓 ∧ [𝐵 / 𝑥]𝜑) ∧ 𝐴 ≠ 𝐵)) → ([𝐵 / 𝑦][𝐴 / 𝑥]((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝑥 ≠ 𝑦) ↔ [𝐵 / 𝑦]((𝜓 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝐴 ≠ 𝑦))) |
32 | | sbcan 3768 |
. . . . . . . . . . . 12
⊢
([𝐵 / 𝑦]((𝜓 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝐴 ≠ 𝑦) ↔ ([𝐵 / 𝑦](𝜓 ∧ [𝑦 / 𝑥]𝜑) ∧ [𝐵 / 𝑦]𝐴 ≠ 𝑦)) |
33 | | sbcan 3768 |
. . . . . . . . . . . . . 14
⊢
([𝐵 / 𝑦](𝜓 ∧ [𝑦 / 𝑥]𝜑) ↔ ([𝐵 / 𝑦]𝜓 ∧ [𝐵 / 𝑦][𝑦 / 𝑥]𝜑)) |
34 | | sbcg 3795 |
. . . . . . . . . . . . . . . 16
⊢ (𝐵 ∈ 𝑋 → ([𝐵 / 𝑦]𝜓 ↔ 𝜓)) |
35 | | sbsbc 3720 |
. . . . . . . . . . . . . . . . . 18
⊢ ([𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑) |
36 | 35 | sbcbii 3776 |
. . . . . . . . . . . . . . . . 17
⊢
([𝐵 / 𝑦][𝑦 / 𝑥]𝜑 ↔ [𝐵 / 𝑦][𝑦 / 𝑥]𝜑) |
37 | | sbccow 3739 |
. . . . . . . . . . . . . . . . . 18
⊢
([𝐵 / 𝑦][𝑦 / 𝑥]𝜑 ↔ [𝐵 / 𝑥]𝜑) |
38 | 37 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐵 ∈ 𝑋 → ([𝐵 / 𝑦][𝑦 / 𝑥]𝜑 ↔ [𝐵 / 𝑥]𝜑)) |
39 | 36, 38 | bitrid 282 |
. . . . . . . . . . . . . . . 16
⊢ (𝐵 ∈ 𝑋 → ([𝐵 / 𝑦][𝑦 / 𝑥]𝜑 ↔ [𝐵 / 𝑥]𝜑)) |
40 | 34, 39 | anbi12d 631 |
. . . . . . . . . . . . . . 15
⊢ (𝐵 ∈ 𝑋 → (([𝐵 / 𝑦]𝜓 ∧ [𝐵 / 𝑦][𝑦 / 𝑥]𝜑) ↔ (𝜓 ∧ [𝐵 / 𝑥]𝜑))) |
41 | 40 | 3ad2ant2 1133 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ((𝜓 ∧ [𝐵 / 𝑥]𝜑) ∧ 𝐴 ≠ 𝐵)) → (([𝐵 / 𝑦]𝜓 ∧ [𝐵 / 𝑦][𝑦 / 𝑥]𝜑) ↔ (𝜓 ∧ [𝐵 / 𝑥]𝜑))) |
42 | 33, 41 | bitrid 282 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ((𝜓 ∧ [𝐵 / 𝑥]𝜑) ∧ 𝐴 ≠ 𝐵)) → ([𝐵 / 𝑦](𝜓 ∧ [𝑦 / 𝑥]𝜑) ↔ (𝜓 ∧ [𝐵 / 𝑥]𝜑))) |
43 | | sbcne12 4346 |
. . . . . . . . . . . . . 14
⊢
([𝐵 / 𝑦]𝐴 ≠ 𝑦 ↔ ⦋𝐵 / 𝑦⦌𝐴 ≠ ⦋𝐵 / 𝑦⦌𝑦) |
44 | | csbconstg 3851 |
. . . . . . . . . . . . . . . 16
⊢ (𝐵 ∈ 𝑋 → ⦋𝐵 / 𝑦⦌𝐴 = 𝐴) |
45 | | csbvarg 4365 |
. . . . . . . . . . . . . . . 16
⊢ (𝐵 ∈ 𝑋 → ⦋𝐵 / 𝑦⦌𝑦 = 𝐵) |
46 | 44, 45 | neeq12d 3005 |
. . . . . . . . . . . . . . 15
⊢ (𝐵 ∈ 𝑋 → (⦋𝐵 / 𝑦⦌𝐴 ≠ ⦋𝐵 / 𝑦⦌𝑦 ↔ 𝐴 ≠ 𝐵)) |
47 | 46 | 3ad2ant2 1133 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ((𝜓 ∧ [𝐵 / 𝑥]𝜑) ∧ 𝐴 ≠ 𝐵)) → (⦋𝐵 / 𝑦⦌𝐴 ≠ ⦋𝐵 / 𝑦⦌𝑦 ↔ 𝐴 ≠ 𝐵)) |
48 | 43, 47 | bitrid 282 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ((𝜓 ∧ [𝐵 / 𝑥]𝜑) ∧ 𝐴 ≠ 𝐵)) → ([𝐵 / 𝑦]𝐴 ≠ 𝑦 ↔ 𝐴 ≠ 𝐵)) |
49 | 42, 48 | anbi12d 631 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ((𝜓 ∧ [𝐵 / 𝑥]𝜑) ∧ 𝐴 ≠ 𝐵)) → (([𝐵 / 𝑦](𝜓 ∧ [𝑦 / 𝑥]𝜑) ∧ [𝐵 / 𝑦]𝐴 ≠ 𝑦) ↔ ((𝜓 ∧ [𝐵 / 𝑥]𝜑) ∧ 𝐴 ≠ 𝐵))) |
50 | 32, 49 | bitrid 282 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ((𝜓 ∧ [𝐵 / 𝑥]𝜑) ∧ 𝐴 ≠ 𝐵)) → ([𝐵 / 𝑦]((𝜓 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝐴 ≠ 𝑦) ↔ ((𝜓 ∧ [𝐵 / 𝑥]𝜑) ∧ 𝐴 ≠ 𝐵))) |
51 | 31, 50 | bitrd 278 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ((𝜓 ∧ [𝐵 / 𝑥]𝜑) ∧ 𝐴 ≠ 𝐵)) → ([𝐵 / 𝑦][𝐴 / 𝑥]((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝑥 ≠ 𝑦) ↔ ((𝜓 ∧ [𝐵 / 𝑥]𝜑) ∧ 𝐴 ≠ 𝐵))) |
52 | 14, 51 | mpbird 256 |
. . . . . . . . 9
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ((𝜓 ∧ [𝐵 / 𝑥]𝜑) ∧ 𝐴 ≠ 𝐵)) → [𝐵 / 𝑦][𝐴 / 𝑥]((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝑥 ≠ 𝑦)) |
53 | | rspesbca 3814 |
. . . . . . . . 9
⊢ ((𝐵 ∈ 𝑋 ∧ [𝐵 / 𝑦][𝐴 / 𝑥]((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝑥 ≠ 𝑦)) → ∃𝑦 ∈ 𝑋 [𝐴 / 𝑥]((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝑥 ≠ 𝑦)) |
54 | 13, 52, 53 | syl2anc 584 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ((𝜓 ∧ [𝐵 / 𝑥]𝜑) ∧ 𝐴 ≠ 𝐵)) → ∃𝑦 ∈ 𝑋 [𝐴 / 𝑥]((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝑥 ≠ 𝑦)) |
55 | | sbcrex 3808 |
. . . . . . . 8
⊢
([𝐴 / 𝑥]∃𝑦 ∈ 𝑋 ((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝑥 ≠ 𝑦) ↔ ∃𝑦 ∈ 𝑋 [𝐴 / 𝑥]((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝑥 ≠ 𝑦)) |
56 | 54, 55 | sylibr 233 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ((𝜓 ∧ [𝐵 / 𝑥]𝜑) ∧ 𝐴 ≠ 𝐵)) → [𝐴 / 𝑥]∃𝑦 ∈ 𝑋 ((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝑥 ≠ 𝑦)) |
57 | | rspesbca 3814 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑋 ∧ [𝐴 / 𝑥]∃𝑦 ∈ 𝑋 ((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝑥 ≠ 𝑦)) → ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑋 ((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝑥 ≠ 𝑦)) |
58 | 12, 56, 57 | syl2anc 584 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ((𝜓 ∧ [𝐵 / 𝑥]𝜑) ∧ 𝐴 ≠ 𝐵)) → ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑋 ((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝑥 ≠ 𝑦)) |
59 | 1, 2, 10, 11, 58 | syl112anc 1373 |
. . . . 5
⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ≠ 𝐵) ∧ (𝜓 ∧ 𝜒)) → ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑋 ((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝑥 ≠ 𝑦)) |
60 | | pm4.61 405 |
. . . . . . 7
⊢ (¬
((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦) ↔ ((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ ¬ 𝑥 = 𝑦)) |
61 | | df-ne 2944 |
. . . . . . . . 9
⊢ (𝑥 ≠ 𝑦 ↔ ¬ 𝑥 = 𝑦) |
62 | 61 | bicomi 223 |
. . . . . . . 8
⊢ (¬
𝑥 = 𝑦 ↔ 𝑥 ≠ 𝑦) |
63 | 62 | anbi2i 623 |
. . . . . . 7
⊢ (((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ ¬ 𝑥 = 𝑦) ↔ ((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝑥 ≠ 𝑦)) |
64 | 60, 63 | bitri 274 |
. . . . . 6
⊢ (¬
((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦) ↔ ((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝑥 ≠ 𝑦)) |
65 | 64 | 2rexbii 3182 |
. . . . 5
⊢
(∃𝑥 ∈
𝑋 ∃𝑦 ∈ 𝑋 ¬ ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦) ↔ ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑋 ((𝜑 ∧ [𝑦 / 𝑥]𝜑) ∧ 𝑥 ≠ 𝑦)) |
66 | 59, 65 | sylibr 233 |
. . . 4
⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ≠ 𝐵) ∧ (𝜓 ∧ 𝜒)) → ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑋 ¬ ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)) |
67 | 66 | olcd 871 |
. . 3
⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ≠ 𝐵) ∧ (𝜓 ∧ 𝜒)) → (¬ ∃𝑥 ∈ 𝑋 𝜑 ∨ ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑋 ¬ ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦))) |
68 | | ianor 979 |
. . . . 5
⊢ (¬
(∃𝑥 ∈ 𝑋 𝜑 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)) ↔ (¬ ∃𝑥 ∈ 𝑋 𝜑 ∨ ¬ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦))) |
69 | | rexnal2 3187 |
. . . . . . 7
⊢
(∃𝑥 ∈
𝑋 ∃𝑦 ∈ 𝑋 ¬ ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦) ↔ ¬ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)) |
70 | 69 | bicomi 223 |
. . . . . 6
⊢ (¬
∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦) ↔ ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑋 ¬ ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)) |
71 | 70 | orbi2i 910 |
. . . . 5
⊢ ((¬
∃𝑥 ∈ 𝑋 𝜑 ∨ ¬ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)) ↔ (¬ ∃𝑥 ∈ 𝑋 𝜑 ∨ ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑋 ¬ ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦))) |
72 | 68, 71 | bitri 274 |
. . . 4
⊢ (¬
(∃𝑥 ∈ 𝑋 𝜑 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)) ↔ (¬ ∃𝑥 ∈ 𝑋 𝜑 ∨ ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑋 ¬ ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦))) |
73 | | reu2 3660 |
. . . 4
⊢
(∃!𝑥 ∈
𝑋 𝜑 ↔ (∃𝑥 ∈ 𝑋 𝜑 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦))) |
74 | 72, 73 | xchnxbir 333 |
. . 3
⊢ (¬
∃!𝑥 ∈ 𝑋 𝜑 ↔ (¬ ∃𝑥 ∈ 𝑋 𝜑 ∨ ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑋 ¬ ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦))) |
75 | 67, 74 | sylibr 233 |
. 2
⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ≠ 𝐵) ∧ (𝜓 ∧ 𝜒)) → ¬ ∃!𝑥 ∈ 𝑋 𝜑) |
76 | 75 | ex 413 |
1
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ≠ 𝐵) → ((𝜓 ∧ 𝜒) → ¬ ∃!𝑥 ∈ 𝑋 𝜑)) |