Proof of Theorem gencbval
Step | Hyp | Ref
| Expression |
1 | | alcom 1458 |
. 2
⊢
(∀𝑥∀𝑦(𝑦 = 𝐴 → (𝜃 → 𝜓)) ↔ ∀𝑦∀𝑥(𝑦 = 𝐴 → (𝜃 → 𝜓))) |
2 | | gencbval.1 |
. . . 4
⊢ 𝐴 ∈ V |
3 | | gencbval.3 |
. . . . . . 7
⊢ (𝐴 = 𝑦 → (𝜒 ↔ 𝜃)) |
4 | | gencbval.2 |
. . . . . . 7
⊢ (𝐴 = 𝑦 → (𝜑 ↔ 𝜓)) |
5 | 3, 4 | imbi12d 233 |
. . . . . 6
⊢ (𝐴 = 𝑦 → ((𝜒 → 𝜑) ↔ (𝜃 → 𝜓))) |
6 | 5 | bicomd 140 |
. . . . 5
⊢ (𝐴 = 𝑦 → ((𝜃 → 𝜓) ↔ (𝜒 → 𝜑))) |
7 | 6 | eqcoms 2160 |
. . . 4
⊢ (𝑦 = 𝐴 → ((𝜃 → 𝜓) ↔ (𝜒 → 𝜑))) |
8 | 2, 7 | ceqsalv 2742 |
. . 3
⊢
(∀𝑦(𝑦 = 𝐴 → (𝜃 → 𝜓)) ↔ (𝜒 → 𝜑)) |
9 | 8 | albii 1450 |
. 2
⊢
(∀𝑥∀𝑦(𝑦 = 𝐴 → (𝜃 → 𝜓)) ↔ ∀𝑥(𝜒 → 𝜑)) |
10 | | 19.23v 1863 |
. . . 4
⊢
(∀𝑥(𝑦 = 𝐴 → (𝜃 → 𝜓)) ↔ (∃𝑥 𝑦 = 𝐴 → (𝜃 → 𝜓))) |
11 | | gencbval.4 |
. . . . . . 7
⊢ (𝜃 ↔ ∃𝑥(𝜒 ∧ 𝐴 = 𝑦)) |
12 | | eqcom 2159 |
. . . . . . . . . 10
⊢ (𝐴 = 𝑦 ↔ 𝑦 = 𝐴) |
13 | 12 | biimpi 119 |
. . . . . . . . 9
⊢ (𝐴 = 𝑦 → 𝑦 = 𝐴) |
14 | 13 | adantl 275 |
. . . . . . . 8
⊢ ((𝜒 ∧ 𝐴 = 𝑦) → 𝑦 = 𝐴) |
15 | 14 | eximi 1580 |
. . . . . . 7
⊢
(∃𝑥(𝜒 ∧ 𝐴 = 𝑦) → ∃𝑥 𝑦 = 𝐴) |
16 | 11, 15 | sylbi 120 |
. . . . . 6
⊢ (𝜃 → ∃𝑥 𝑦 = 𝐴) |
17 | | pm2.04 82 |
. . . . . 6
⊢
((∃𝑥 𝑦 = 𝐴 → (𝜃 → 𝜓)) → (𝜃 → (∃𝑥 𝑦 = 𝐴 → 𝜓))) |
18 | 16, 17 | mpdi 43 |
. . . . 5
⊢
((∃𝑥 𝑦 = 𝐴 → (𝜃 → 𝜓)) → (𝜃 → 𝜓)) |
19 | | ax-1 6 |
. . . . 5
⊢ ((𝜃 → 𝜓) → (∃𝑥 𝑦 = 𝐴 → (𝜃 → 𝜓))) |
20 | 18, 19 | impbii 125 |
. . . 4
⊢
((∃𝑥 𝑦 = 𝐴 → (𝜃 → 𝜓)) ↔ (𝜃 → 𝜓)) |
21 | 10, 20 | bitri 183 |
. . 3
⊢
(∀𝑥(𝑦 = 𝐴 → (𝜃 → 𝜓)) ↔ (𝜃 → 𝜓)) |
22 | 21 | albii 1450 |
. 2
⊢
(∀𝑦∀𝑥(𝑦 = 𝐴 → (𝜃 → 𝜓)) ↔ ∀𝑦(𝜃 → 𝜓)) |
23 | 1, 9, 22 | 3bitr3i 209 |
1
⊢
(∀𝑥(𝜒 → 𝜑) ↔ ∀𝑦(𝜃 → 𝜓)) |