Proof of Theorem rspct
| Step | Hyp | Ref
| Expression |
| 1 | | df-ral 3062 |
. . . 4
⊢
(∀𝑥 ∈
𝐵 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝜑)) |
| 2 | | eleq1 2829 |
. . . . . . . . . 10
⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵)) |
| 3 | 2 | adantr 480 |
. . . . . . . . 9
⊢ ((𝑥 = 𝐴 ∧ (𝜑 ↔ 𝜓)) → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵)) |
| 4 | | simpr 484 |
. . . . . . . . 9
⊢ ((𝑥 = 𝐴 ∧ (𝜑 ↔ 𝜓)) → (𝜑 ↔ 𝜓)) |
| 5 | 3, 4 | imbi12d 344 |
. . . . . . . 8
⊢ ((𝑥 = 𝐴 ∧ (𝜑 ↔ 𝜓)) → ((𝑥 ∈ 𝐵 → 𝜑) ↔ (𝐴 ∈ 𝐵 → 𝜓))) |
| 6 | 5 | ex 412 |
. . . . . . 7
⊢ (𝑥 = 𝐴 → ((𝜑 ↔ 𝜓) → ((𝑥 ∈ 𝐵 → 𝜑) ↔ (𝐴 ∈ 𝐵 → 𝜓)))) |
| 7 | 6 | a2i 14 |
. . . . . 6
⊢ ((𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) → (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 → 𝜑) ↔ (𝐴 ∈ 𝐵 → 𝜓)))) |
| 8 | 7 | alimi 1811 |
. . . . 5
⊢
(∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) → ∀𝑥(𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 → 𝜑) ↔ (𝐴 ∈ 𝐵 → 𝜓)))) |
| 9 | | nfv 1914 |
. . . . . . 7
⊢
Ⅎ𝑥 𝐴 ∈ 𝐵 |
| 10 | | rspct.1 |
. . . . . . 7
⊢
Ⅎ𝑥𝜓 |
| 11 | 9, 10 | nfim 1896 |
. . . . . 6
⊢
Ⅎ𝑥(𝐴 ∈ 𝐵 → 𝜓) |
| 12 | | nfcv 2905 |
. . . . . 6
⊢
Ⅎ𝑥𝐴 |
| 13 | 11, 12 | spcgft 3549 |
. . . . 5
⊢
(∀𝑥(𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 → 𝜑) ↔ (𝐴 ∈ 𝐵 → 𝜓))) → (𝐴 ∈ 𝐵 → (∀𝑥(𝑥 ∈ 𝐵 → 𝜑) → (𝐴 ∈ 𝐵 → 𝜓)))) |
| 14 | 8, 13 | syl 17 |
. . . 4
⊢
(∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) → (𝐴 ∈ 𝐵 → (∀𝑥(𝑥 ∈ 𝐵 → 𝜑) → (𝐴 ∈ 𝐵 → 𝜓)))) |
| 15 | 1, 14 | syl7bi 255 |
. . 3
⊢
(∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) → (𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → (𝐴 ∈ 𝐵 → 𝜓)))) |
| 16 | 15 | com34 91 |
. 2
⊢
(∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) → (𝐴 ∈ 𝐵 → (𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → 𝜓)))) |
| 17 | 16 | pm2.43d 53 |
1
⊢
(∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) → (𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → 𝜓))) |