Proof of Theorem rexrsb
Step | Hyp | Ref
| Expression |
1 | | rexsb 41168 |
. 2
⊢
(∃𝑥 ∈
𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐴 ∀𝑥(𝑥 = 𝑦 → 𝜑)) |
2 | | alral 2928 |
. . . 4
⊢
(∀𝑥(𝑥 = 𝑦 → 𝜑) → ∀𝑥 ∈ 𝐴 (𝑥 = 𝑦 → 𝜑)) |
3 | | df-ral 2917 |
. . . . . 6
⊢
(∀𝑥 ∈
𝐴 (𝑥 = 𝑦 → 𝜑) ↔ ∀𝑥(𝑥 ∈ 𝐴 → (𝑥 = 𝑦 → 𝜑))) |
4 | | 19.27v 1908 |
. . . . . . . 8
⊢
(∀𝑥((𝑥 ∈ 𝐴 → (𝑥 = 𝑦 → 𝜑)) ∧ 𝑦 ∈ 𝐴) ↔ (∀𝑥(𝑥 ∈ 𝐴 → (𝑥 = 𝑦 → 𝜑)) ∧ 𝑦 ∈ 𝐴)) |
5 | | pm2.04 90 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ 𝐴 → (𝑥 = 𝑦 → 𝜑)) → (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 → 𝜑))) |
6 | | eleq1 2689 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴)) |
7 | 6 | biimprd 238 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑦 → (𝑦 ∈ 𝐴 → 𝑥 ∈ 𝐴)) |
8 | | pm2.83 84 |
. . . . . . . . . . . 12
⊢ ((𝑥 = 𝑦 → (𝑦 ∈ 𝐴 → 𝑥 ∈ 𝐴)) → ((𝑥 = 𝑦 → (𝑥 ∈ 𝐴 → 𝜑)) → (𝑥 = 𝑦 → (𝑦 ∈ 𝐴 → 𝜑)))) |
9 | 7, 8 | ax-mp 5 |
. . . . . . . . . . 11
⊢ ((𝑥 = 𝑦 → (𝑥 ∈ 𝐴 → 𝜑)) → (𝑥 = 𝑦 → (𝑦 ∈ 𝐴 → 𝜑))) |
10 | | pm2.04 90 |
. . . . . . . . . . 11
⊢ ((𝑥 = 𝑦 → (𝑦 ∈ 𝐴 → 𝜑)) → (𝑦 ∈ 𝐴 → (𝑥 = 𝑦 → 𝜑))) |
11 | 5, 9, 10 | 3syl 18 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ 𝐴 → (𝑥 = 𝑦 → 𝜑)) → (𝑦 ∈ 𝐴 → (𝑥 = 𝑦 → 𝜑))) |
12 | 11 | imp 445 |
. . . . . . . . 9
⊢ (((𝑥 ∈ 𝐴 → (𝑥 = 𝑦 → 𝜑)) ∧ 𝑦 ∈ 𝐴) → (𝑥 = 𝑦 → 𝜑)) |
13 | 12 | alimi 1739 |
. . . . . . . 8
⊢
(∀𝑥((𝑥 ∈ 𝐴 → (𝑥 = 𝑦 → 𝜑)) ∧ 𝑦 ∈ 𝐴) → ∀𝑥(𝑥 = 𝑦 → 𝜑)) |
14 | 4, 13 | sylbir 225 |
. . . . . . 7
⊢
((∀𝑥(𝑥 ∈ 𝐴 → (𝑥 = 𝑦 → 𝜑)) ∧ 𝑦 ∈ 𝐴) → ∀𝑥(𝑥 = 𝑦 → 𝜑)) |
15 | 14 | ex 450 |
. . . . . 6
⊢
(∀𝑥(𝑥 ∈ 𝐴 → (𝑥 = 𝑦 → 𝜑)) → (𝑦 ∈ 𝐴 → ∀𝑥(𝑥 = 𝑦 → 𝜑))) |
16 | 3, 15 | sylbi 207 |
. . . . 5
⊢
(∀𝑥 ∈
𝐴 (𝑥 = 𝑦 → 𝜑) → (𝑦 ∈ 𝐴 → ∀𝑥(𝑥 = 𝑦 → 𝜑))) |
17 | 16 | com12 32 |
. . . 4
⊢ (𝑦 ∈ 𝐴 → (∀𝑥 ∈ 𝐴 (𝑥 = 𝑦 → 𝜑) → ∀𝑥(𝑥 = 𝑦 → 𝜑))) |
18 | 2, 17 | impbid2 216 |
. . 3
⊢ (𝑦 ∈ 𝐴 → (∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ ∀𝑥 ∈ 𝐴 (𝑥 = 𝑦 → 𝜑))) |
19 | 18 | rexbiia 3040 |
. 2
⊢
(∃𝑦 ∈
𝐴 ∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ ∃𝑦 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (𝑥 = 𝑦 → 𝜑)) |
20 | 1, 19 | bitri 264 |
1
⊢
(∃𝑥 ∈
𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (𝑥 = 𝑦 → 𝜑)) |