Proof of Theorem rexrsb
Step | Hyp | Ref
| Expression |
1 | | rexsb 39817 |
. 2
⊢
(∃𝑥 ∈
𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐴 ∀𝑥(𝑥 = 𝑦 → 𝜑)) |
2 | | alral 2912 |
. . . 4
⊢
(∀𝑥(𝑥 = 𝑦 → 𝜑) → ∀𝑥 ∈ 𝐴 (𝑥 = 𝑦 → 𝜑)) |
3 | | df-ral 2901 |
. . . . . 6
⊢
(∀𝑥 ∈
𝐴 (𝑥 = 𝑦 → 𝜑) ↔ ∀𝑥(𝑥 ∈ 𝐴 → (𝑥 = 𝑦 → 𝜑))) |
4 | | 19.27v 1895 |
. . . . . . . 8
⊢
(∀𝑥((𝑥 ∈ 𝐴 → (𝑥 = 𝑦 → 𝜑)) ∧ 𝑦 ∈ 𝐴) ↔ (∀𝑥(𝑥 ∈ 𝐴 → (𝑥 = 𝑦 → 𝜑)) ∧ 𝑦 ∈ 𝐴)) |
5 | | pm2.04 88 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ 𝐴 → (𝑥 = 𝑦 → 𝜑)) → (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 → 𝜑))) |
6 | | eleq1 2676 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴)) |
7 | 6 | biimprd 237 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑦 → (𝑦 ∈ 𝐴 → 𝑥 ∈ 𝐴)) |
8 | | pm2.83 82 |
. . . . . . . . . . . 12
⊢ ((𝑥 = 𝑦 → (𝑦 ∈ 𝐴 → 𝑥 ∈ 𝐴)) → ((𝑥 = 𝑦 → (𝑥 ∈ 𝐴 → 𝜑)) → (𝑥 = 𝑦 → (𝑦 ∈ 𝐴 → 𝜑)))) |
9 | 7, 8 | ax-mp 5 |
. . . . . . . . . . 11
⊢ ((𝑥 = 𝑦 → (𝑥 ∈ 𝐴 → 𝜑)) → (𝑥 = 𝑦 → (𝑦 ∈ 𝐴 → 𝜑))) |
10 | | pm2.04 88 |
. . . . . . . . . . 11
⊢ ((𝑥 = 𝑦 → (𝑦 ∈ 𝐴 → 𝜑)) → (𝑦 ∈ 𝐴 → (𝑥 = 𝑦 → 𝜑))) |
11 | 5, 9, 10 | 3syl 18 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ 𝐴 → (𝑥 = 𝑦 → 𝜑)) → (𝑦 ∈ 𝐴 → (𝑥 = 𝑦 → 𝜑))) |
12 | 11 | imp 444 |
. . . . . . . . 9
⊢ (((𝑥 ∈ 𝐴 → (𝑥 = 𝑦 → 𝜑)) ∧ 𝑦 ∈ 𝐴) → (𝑥 = 𝑦 → 𝜑)) |
13 | 12 | alimi 1730 |
. . . . . . . 8
⊢
(∀𝑥((𝑥 ∈ 𝐴 → (𝑥 = 𝑦 → 𝜑)) ∧ 𝑦 ∈ 𝐴) → ∀𝑥(𝑥 = 𝑦 → 𝜑)) |
14 | 4, 13 | sylbir 224 |
. . . . . . 7
⊢
((∀𝑥(𝑥 ∈ 𝐴 → (𝑥 = 𝑦 → 𝜑)) ∧ 𝑦 ∈ 𝐴) → ∀𝑥(𝑥 = 𝑦 → 𝜑)) |
15 | 14 | ex 449 |
. . . . . 6
⊢
(∀𝑥(𝑥 ∈ 𝐴 → (𝑥 = 𝑦 → 𝜑)) → (𝑦 ∈ 𝐴 → ∀𝑥(𝑥 = 𝑦 → 𝜑))) |
16 | 3, 15 | sylbi 206 |
. . . . 5
⊢
(∀𝑥 ∈
𝐴 (𝑥 = 𝑦 → 𝜑) → (𝑦 ∈ 𝐴 → ∀𝑥(𝑥 = 𝑦 → 𝜑))) |
17 | 16 | com12 32 |
. . . 4
⊢ (𝑦 ∈ 𝐴 → (∀𝑥 ∈ 𝐴 (𝑥 = 𝑦 → 𝜑) → ∀𝑥(𝑥 = 𝑦 → 𝜑))) |
18 | 2, 17 | impbid2 215 |
. . 3
⊢ (𝑦 ∈ 𝐴 → (∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ ∀𝑥 ∈ 𝐴 (𝑥 = 𝑦 → 𝜑))) |
19 | 18 | rexbiia 3022 |
. 2
⊢
(∃𝑦 ∈
𝐴 ∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ ∃𝑦 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (𝑥 = 𝑦 → 𝜑)) |
20 | 1, 19 | bitri 263 |
1
⊢
(∃𝑥 ∈
𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (𝑥 = 𝑦 → 𝜑)) |