Proof of Theorem bj-rspgt
Step | Hyp | Ref
| Expression |
1 | | eleq1 2220 |
. . . . . . . . 9
⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵)) |
2 | 1 | imbi1d 230 |
. . . . . . . 8
⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → 𝜑)) ↔ (𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → 𝜑)))) |
3 | 2 | biimpd 143 |
. . . . . . 7
⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → 𝜑)) → (𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → 𝜑)))) |
4 | | imim2 55 |
. . . . . . . 8
⊢ ((𝜑 → 𝜓) → ((∀𝑥 ∈ 𝐵 𝜑 → 𝜑) → (∀𝑥 ∈ 𝐵 𝜑 → 𝜓))) |
5 | 4 | imim2d 54 |
. . . . . . 7
⊢ ((𝜑 → 𝜓) → ((𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → 𝜑)) → (𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → 𝜓)))) |
6 | 3, 5 | syl9 72 |
. . . . . 6
⊢ (𝑥 = 𝐴 → ((𝜑 → 𝜓) → ((𝑥 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → 𝜑)) → (𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → 𝜓))))) |
7 | 6 | a2i 11 |
. . . . 5
⊢ ((𝑥 = 𝐴 → (𝜑 → 𝜓)) → (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → 𝜑)) → (𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → 𝜓))))) |
8 | 7 | alimi 1435 |
. . . 4
⊢
(∀𝑥(𝑥 = 𝐴 → (𝜑 → 𝜓)) → ∀𝑥(𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → 𝜑)) → (𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → 𝜓))))) |
9 | | bj-rspg.nfa |
. . . . 5
⊢
Ⅎ𝑥𝐴 |
10 | | bj-rspg.nfb |
. . . . . . 7
⊢
Ⅎ𝑥𝐵 |
11 | 9, 10 | nfel 2308 |
. . . . . 6
⊢
Ⅎ𝑥 𝐴 ∈ 𝐵 |
12 | | nfra1 2488 |
. . . . . . 7
⊢
Ⅎ𝑥∀𝑥 ∈ 𝐵 𝜑 |
13 | | bj-rspg.nf2 |
. . . . . . 7
⊢
Ⅎ𝑥𝜓 |
14 | 12, 13 | nfim 1552 |
. . . . . 6
⊢
Ⅎ𝑥(∀𝑥 ∈ 𝐵 𝜑 → 𝜓) |
15 | 11, 14 | nfim 1552 |
. . . . 5
⊢
Ⅎ𝑥(𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → 𝜓)) |
16 | | rsp 2504 |
. . . . . . 7
⊢
(∀𝑥 ∈
𝐵 𝜑 → (𝑥 ∈ 𝐵 → 𝜑)) |
17 | 16 | a1i 9 |
. . . . . 6
⊢ (𝑥 = 𝐴 → (∀𝑥 ∈ 𝐵 𝜑 → (𝑥 ∈ 𝐵 → 𝜑))) |
18 | 17 | com23 78 |
. . . . 5
⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → 𝜑))) |
19 | 9, 15, 18 | bj-vtoclgft 13360 |
. . . 4
⊢
(∀𝑥(𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → 𝜑)) → (𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → 𝜓)))) → (𝐴 ∈ 𝐵 → (𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → 𝜓)))) |
20 | 8, 19 | syl 14 |
. . 3
⊢
(∀𝑥(𝑥 = 𝐴 → (𝜑 → 𝜓)) → (𝐴 ∈ 𝐵 → (𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → 𝜓)))) |
21 | 20 | pm2.43d 50 |
. 2
⊢
(∀𝑥(𝑥 = 𝐴 → (𝜑 → 𝜓)) → (𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → 𝜓))) |
22 | 21 | com23 78 |
1
⊢
(∀𝑥(𝑥 = 𝐴 → (𝜑 → 𝜓)) → (∀𝑥 ∈ 𝐵 𝜑 → (𝐴 ∈ 𝐵 → 𝜓))) |