Proof of Theorem rspct
Step | Hyp | Ref
| Expression |
1 | | df-ral 2619 |
. . . 4
⊢ (∀x ∈ B φ ↔ ∀x(x ∈ B → φ)) |
2 | | eleq1 2413 |
. . . . . . . . . 10
⊢ (x = A →
(x ∈
B ↔ A ∈ B)) |
3 | 2 | adantr 451 |
. . . . . . . . 9
⊢ ((x = A ∧ (φ ↔
ψ)) → (x ∈ B ↔ A ∈ B)) |
4 | | simpr 447 |
. . . . . . . . 9
⊢ ((x = A ∧ (φ ↔
ψ)) → (φ ↔ ψ)) |
5 | 3, 4 | imbi12d 311 |
. . . . . . . 8
⊢ ((x = A ∧ (φ ↔
ψ)) → ((x ∈ B → φ)
↔ (A ∈ B →
ψ))) |
6 | 5 | ex 423 |
. . . . . . 7
⊢ (x = A →
((φ ↔ ψ) → ((x ∈ B → φ)
↔ (A ∈ B →
ψ)))) |
7 | 6 | a2i 12 |
. . . . . 6
⊢ ((x = A →
(φ ↔ ψ)) → (x = A →
((x ∈
B → φ) ↔ (A ∈ B → ψ)))) |
8 | 7 | alimi 1559 |
. . . . 5
⊢ (∀x(x = A →
(φ ↔ ψ)) → ∀x(x = A →
((x ∈
B → φ) ↔ (A ∈ B → ψ)))) |
9 | | nfv 1619 |
. . . . . . 7
⊢ Ⅎx A ∈ B |
10 | | rspct.1 |
. . . . . . 7
⊢ Ⅎxψ |
11 | 9, 10 | nfim 1813 |
. . . . . 6
⊢ Ⅎx(A ∈ B →
ψ) |
12 | | nfcv 2489 |
. . . . . 6
⊢
ℲxA |
13 | 11, 12 | spcgft 2931 |
. . . . 5
⊢ (∀x(x = A →
((x ∈
B → φ) ↔ (A ∈ B → ψ))) → (A ∈ B → (∀x(x ∈ B → φ)
→ (A ∈ B →
ψ)))) |
14 | 8, 13 | syl 15 |
. . . 4
⊢ (∀x(x = A →
(φ ↔ ψ)) → (A ∈ B → (∀x(x ∈ B → φ)
→ (A ∈ B →
ψ)))) |
15 | 1, 14 | syl7bi 221 |
. . 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 φ → ψ))) |