Proof of Theorem bj-rspgt
Step | Hyp | Ref
| Expression |
1 | | eleq1 2097 |
. . . . . . . . 9
⊢ (x = A →
(x ∈
B ↔ A ∈ B)) |
2 | 1 | imbi1d 220 |
. . . . . . . 8
⊢ (x = A →
((x ∈
B → (∀x ∈ B φ → φ)) ↔ (A ∈ B → (∀x ∈ B φ → φ)))) |
3 | 2 | biimpd 132 |
. . . . . . 7
⊢ (x = A →
((x ∈
B → (∀x ∈ B φ → φ)) → (A ∈ B → (∀x ∈ B φ → φ)))) |
4 | | imim2 49 |
. . . . . . . 8
⊢ ((φ → ψ) → ((∀x ∈ B φ → φ) → (∀x ∈ B φ → ψ))) |
5 | 4 | imim2d 48 |
. . . . . . 7
⊢ ((φ → ψ) → ((A ∈ B → (∀x ∈ B φ → φ)) → (A ∈ B → (∀x ∈ B φ → ψ)))) |
6 | 3, 5 | syl9 66 |
. . . . . 6
⊢ (x = A →
((φ → ψ) → ((x ∈ B → (∀x ∈ B φ → φ)) → (A ∈ B → (∀x ∈ B φ → ψ))))) |
7 | 6 | a2i 11 |
. . . . 5
⊢
((x = A → (φ
→ ψ)) → (x = A →
((x ∈
B → (∀x ∈ B φ → φ)) → (A ∈ B → (∀x ∈ B φ → ψ))))) |
8 | 7 | alimi 1341 |
. . . 4
⊢ (∀x(x = A →
(φ → ψ)) → ∀x(x = A →
((x ∈
B → (∀x ∈ B φ → φ)) → (A ∈ B → (∀x ∈ B φ → ψ))))) |
9 | | bj-rspg.nfa |
. . . . 5
⊢
ℲxA |
10 | | bj-rspg.nfb |
. . . . . . 7
⊢
ℲxB |
11 | 9, 10 | nfel 2183 |
. . . . . 6
⊢
Ⅎx A ∈ B |
12 | | nfra1 2349 |
. . . . . . 7
⊢
Ⅎx∀x ∈ B φ |
13 | | bj-rspg.nf2 |
. . . . . . 7
⊢
Ⅎxψ |
14 | 12, 13 | nfim 1461 |
. . . . . 6
⊢
Ⅎx(∀x ∈ B φ → ψ) |
15 | 11, 14 | nfim 1461 |
. . . . 5
⊢
Ⅎx(A ∈ B → (∀x ∈ B φ → ψ)) |
16 | | rsp 2363 |
. . . . . . 7
⊢ (∀x ∈ B φ → (x ∈ B → φ)) |
17 | 16 | a1i 9 |
. . . . . 6
⊢ (x = A →
(∀x
∈ B φ → (x ∈ B → φ))) |
18 | 17 | com23 72 |
. . . . 5
⊢ (x = A →
(x ∈
B → (∀x ∈ B φ → φ))) |
19 | 9, 15, 18 | bj-vtoclgft 9249 |
. . . 4
⊢ (∀x(x = A →
((x ∈
B → (∀x ∈ B φ → φ)) → (A ∈ B → (∀x ∈ B φ → ψ)))) → (A ∈ B → (A
∈ B
→ (∀x ∈ B φ →
ψ)))) |
20 | 8, 19 | syl 14 |
. . 3
⊢ (∀x(x = A →
(φ → ψ)) → (A ∈ B → (A
∈ B
→ (∀x ∈ B φ →
ψ)))) |
21 | 20 | pm2.43d 44 |
. 2
⊢ (∀x(x = A →
(φ → ψ)) → (A ∈ B → (∀x ∈ B φ → ψ))) |
22 | 21 | com23 72 |
1
⊢ (∀x(x = A →
(φ → ψ)) → (∀x ∈ B φ → (A ∈ B → ψ))) |