Proof of Theorem ceqsalt
Step | Hyp | Ref
| Expression |
1 | | biimp 214 |
. . . . . . 7
⊢ ((𝜑 ↔ 𝜓) → (𝜑 → 𝜓)) |
2 | 1 | imim3i 64 |
. . . . . 6
⊢ ((𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) → ((𝑥 = 𝐴 → 𝜑) → (𝑥 = 𝐴 → 𝜓))) |
3 | 2 | al2imi 1818 |
. . . . 5
⊢
(∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) → (∀𝑥(𝑥 = 𝐴 → 𝜑) → ∀𝑥(𝑥 = 𝐴 → 𝜓))) |
4 | | elisset 2816 |
. . . . . 6
⊢ (𝐴 ∈ 𝑉 → ∃𝑥 𝑥 = 𝐴) |
5 | | 19.23t 2204 |
. . . . . . 7
⊢
(Ⅎ𝑥𝜓 → (∀𝑥(𝑥 = 𝐴 → 𝜓) ↔ (∃𝑥 𝑥 = 𝐴 → 𝜓))) |
6 | 5 | biimpd 228 |
. . . . . 6
⊢
(Ⅎ𝑥𝜓 → (∀𝑥(𝑥 = 𝐴 → 𝜓) → (∃𝑥 𝑥 = 𝐴 → 𝜓))) |
7 | 4, 6 | syl7 74 |
. . . . 5
⊢
(Ⅎ𝑥𝜓 → (∀𝑥(𝑥 = 𝐴 → 𝜓) → (𝐴 ∈ 𝑉 → 𝜓))) |
8 | 3, 7 | sylan9r 510 |
. . . 4
⊢
((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓))) → (∀𝑥(𝑥 = 𝐴 → 𝜑) → (𝐴 ∈ 𝑉 → 𝜓))) |
9 | 8 | com23 86 |
. . 3
⊢
((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓))) → (𝐴 ∈ 𝑉 → (∀𝑥(𝑥 = 𝐴 → 𝜑) → 𝜓))) |
10 | 9 | 3impia 1118 |
. 2
⊢
((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ 𝐴 ∈ 𝑉) → (∀𝑥(𝑥 = 𝐴 → 𝜑) → 𝜓)) |
11 | | biimpr 219 |
. . . . . . . 8
⊢ ((𝜑 ↔ 𝜓) → (𝜓 → 𝜑)) |
12 | 11 | imim2i 16 |
. . . . . . 7
⊢ ((𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) → (𝑥 = 𝐴 → (𝜓 → 𝜑))) |
13 | 12 | com23 86 |
. . . . . 6
⊢ ((𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) → (𝜓 → (𝑥 = 𝐴 → 𝜑))) |
14 | 13 | alimi 1814 |
. . . . 5
⊢
(∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) → ∀𝑥(𝜓 → (𝑥 = 𝐴 → 𝜑))) |
15 | | 19.21t 2200 |
. . . . 5
⊢
(Ⅎ𝑥𝜓 → (∀𝑥(𝜓 → (𝑥 = 𝐴 → 𝜑)) ↔ (𝜓 → ∀𝑥(𝑥 = 𝐴 → 𝜑)))) |
16 | 14, 15 | imbitrid 243 |
. . . 4
⊢
(Ⅎ𝑥𝜓 → (∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) → (𝜓 → ∀𝑥(𝑥 = 𝐴 → 𝜑)))) |
17 | 16 | imp 408 |
. . 3
⊢
((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓))) → (𝜓 → ∀𝑥(𝑥 = 𝐴 → 𝜑))) |
18 | 17 | 3adant3 1133 |
. 2
⊢
((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ 𝐴 ∈ 𝑉) → (𝜓 → ∀𝑥(𝑥 = 𝐴 → 𝜑))) |
19 | 10, 18 | impbid 211 |
1
⊢
((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ 𝐴 ∈ 𝑉) → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓)) |