Proof of Theorem rspct
Step | Hyp | Ref
| Expression |
1 | | df-ral 3071 |
. . . 4
⊢
(∀𝑥 ∈
𝐵 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝜑)) |
2 | | eleq1 2828 |
. . . . . . . . . 10
⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵)) |
3 | 2 | adantr 481 |
. . . . . . . . 9
⊢ ((𝑥 = 𝐴 ∧ (𝜑 ↔ 𝜓)) → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵)) |
4 | | simpr 485 |
. . . . . . . . 9
⊢ ((𝑥 = 𝐴 ∧ (𝜑 ↔ 𝜓)) → (𝜑 ↔ 𝜓)) |
5 | 3, 4 | imbi12d 345 |
. . . . . . . 8
⊢ ((𝑥 = 𝐴 ∧ (𝜑 ↔ 𝜓)) → ((𝑥 ∈ 𝐵 → 𝜑) ↔ (𝐴 ∈ 𝐵 → 𝜓))) |
6 | 5 | ex 413 |
. . . . . . 7
⊢ (𝑥 = 𝐴 → ((𝜑 ↔ 𝜓) → ((𝑥 ∈ 𝐵 → 𝜑) ↔ (𝐴 ∈ 𝐵 → 𝜓)))) |
7 | 6 | a2i 14 |
. . . . . 6
⊢ ((𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) → (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 → 𝜑) ↔ (𝐴 ∈ 𝐵 → 𝜓)))) |
8 | 7 | alimi 1818 |
. . . . 5
⊢
(∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) → ∀𝑥(𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 → 𝜑) ↔ (𝐴 ∈ 𝐵 → 𝜓)))) |
9 | | nfv 1921 |
. . . . . . 7
⊢
Ⅎ𝑥 𝐴 ∈ 𝐵 |
10 | | rspct.1 |
. . . . . . 7
⊢
Ⅎ𝑥𝜓 |
11 | 9, 10 | nfim 1903 |
. . . . . 6
⊢
Ⅎ𝑥(𝐴 ∈ 𝐵 → 𝜓) |
12 | | nfcv 2909 |
. . . . . 6
⊢
Ⅎ𝑥𝐴 |
13 | 11, 12 | spcgft 3526 |
. . . . 5
⊢
(∀𝑥(𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 → 𝜑) ↔ (𝐴 ∈ 𝐵 → 𝜓))) → (𝐴 ∈ 𝐵 → (∀𝑥(𝑥 ∈ 𝐵 → 𝜑) → (𝐴 ∈ 𝐵 → 𝜓)))) |
14 | 8, 13 | syl 17 |
. . . 4
⊢
(∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) → (𝐴 ∈ 𝐵 → (∀𝑥(𝑥 ∈ 𝐵 → 𝜑) → (𝐴 ∈ 𝐵 → 𝜓)))) |
15 | 1, 14 | syl7bi 254 |
. . 3
⊢
(∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) → (𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → (𝐴 ∈ 𝐵 → 𝜓)))) |
16 | 15 | com34 91 |
. 2
⊢
(∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) → (𝐴 ∈ 𝐵 → (𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → 𝜓)))) |
17 | 16 | pm2.43d 53 |
1
⊢
(∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) → (𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → 𝜓))) |