Proof of Theorem rspct
Step | Hyp | Ref
| Expression |
1 | | df-ral 2305 |
. . . 4
⊢ (∀x ∈ B φ ↔ ∀x(x ∈ B → φ)) |
2 | | eleq1 2097 |
. . . . . . . . . 10
⊢ (x = A →
(x ∈
B ↔ A ∈ B)) |
3 | 2 | adantr 261 |
. . . . . . . . 9
⊢
((x = A ∧ (φ ↔ ψ)) → (x ∈ B ↔ A ∈ B)) |
4 | | simpr 103 |
. . . . . . . . 9
⊢
((x = A ∧ (φ ↔ ψ)) → (φ ↔ ψ)) |
5 | 3, 4 | imbi12d 223 |
. . . . . . . 8
⊢
((x = A ∧ (φ ↔ ψ)) → ((x ∈ B → φ)
↔ (A ∈ B →
ψ))) |
6 | 5 | ex 108 |
. . . . . . 7
⊢ (x = A →
((φ ↔ ψ) → ((x ∈ B → φ)
↔ (A ∈ B →
ψ)))) |
7 | 6 | a2i 11 |
. . . . . 6
⊢
((x = A → (φ
↔ ψ)) → (x = A →
((x ∈
B → φ) ↔ (A ∈ B → ψ)))) |
8 | 7 | alimi 1341 |
. . . . 5
⊢ (∀x(x = A →
(φ ↔ ψ)) → ∀x(x = A →
((x ∈
B → φ) ↔ (A ∈ B → ψ)))) |
9 | | nfv 1418 |
. . . . . . 7
⊢
Ⅎx A ∈ B |
10 | | rspct.1 |
. . . . . . 7
⊢
Ⅎxψ |
11 | 9, 10 | nfim 1461 |
. . . . . 6
⊢
Ⅎx(A ∈ B → ψ) |
12 | | nfcv 2175 |
. . . . . 6
⊢
ℲxA |
13 | 11, 12 | spcgft 2624 |
. . . . 5
⊢ (∀x(x = A →
((x ∈
B → φ) ↔ (A ∈ B → ψ))) → (A ∈ B → (∀x(x ∈ B → φ)
→ (A ∈ B →
ψ)))) |
14 | 8, 13 | syl 14 |
. . . 4
⊢ (∀x(x = A →
(φ ↔ ψ)) → (A ∈ B → (∀x(x ∈ B → φ)
→ (A ∈ B →
ψ)))) |
15 | 1, 14 | syl7bi 154 |
. . 3
⊢ (∀x(x = A →
(φ ↔ ψ)) → (A ∈ B → (∀x ∈ B φ → (A ∈ B → ψ)))) |
16 | 15 | com34 77 |
. 2
⊢ (∀x(x = A →
(φ ↔ ψ)) → (A ∈ B → (A
∈ B
→ (∀x ∈ B φ →
ψ)))) |
17 | 16 | pm2.43d 44 |
1
⊢ (∀x(x = A →
(φ ↔ ψ)) → (A ∈ B → (∀x ∈ B φ → ψ))) |