Step | Hyp | Ref
| Expression |
1 | | df-ral 2458 |
. . . 4
⊢
(∀𝑥 ∈
𝐵 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝜑)) |
2 | | eleq1 2238 |
. . . . . . . . . 10
⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵)) |
3 | 2 | adantr 276 |
. . . . . . . . 9
⊢ ((𝑥 = 𝐴 ∧ (𝜑 ↔ 𝜓)) → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵)) |
4 | | simpr 110 |
. . . . . . . . 9
⊢ ((𝑥 = 𝐴 ∧ (𝜑 ↔ 𝜓)) → (𝜑 ↔ 𝜓)) |
5 | 3, 4 | imbi12d 234 |
. . . . . . . 8
⊢ ((𝑥 = 𝐴 ∧ (𝜑 ↔ 𝜓)) → ((𝑥 ∈ 𝐵 → 𝜑) ↔ (𝐴 ∈ 𝐵 → 𝜓))) |
6 | 5 | ex 115 |
. . . . . . 7
⊢ (𝑥 = 𝐴 → ((𝜑 ↔ 𝜓) → ((𝑥 ∈ 𝐵 → 𝜑) ↔ (𝐴 ∈ 𝐵 → 𝜓)))) |
7 | 6 | a2i 11 |
. . . . . 6
⊢ ((𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) → (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 → 𝜑) ↔ (𝐴 ∈ 𝐵 → 𝜓)))) |
8 | 7 | alimi 1453 |
. . . . 5
⊢
(∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) → ∀𝑥(𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 → 𝜑) ↔ (𝐴 ∈ 𝐵 → 𝜓)))) |
9 | | nfv 1526 |
. . . . . . 7
⊢
Ⅎ𝑥 𝐴 ∈ 𝐵 |
10 | | rspct.1 |
. . . . . . 7
⊢
Ⅎ𝑥𝜓 |
11 | 9, 10 | nfim 1570 |
. . . . . 6
⊢
Ⅎ𝑥(𝐴 ∈ 𝐵 → 𝜓) |
12 | | nfcv 2317 |
. . . . . 6
⊢
Ⅎ𝑥𝐴 |
13 | 11, 12 | spcgft 2812 |
. . . . 5
⊢
(∀𝑥(𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 → 𝜑) ↔ (𝐴 ∈ 𝐵 → 𝜓))) → (𝐴 ∈ 𝐵 → (∀𝑥(𝑥 ∈ 𝐵 → 𝜑) → (𝐴 ∈ 𝐵 → 𝜓)))) |
14 | 8, 13 | syl 14 |
. . . 4
⊢
(∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) → (𝐴 ∈ 𝐵 → (∀𝑥(𝑥 ∈ 𝐵 → 𝜑) → (𝐴 ∈ 𝐵 → 𝜓)))) |
15 | 1, 14 | syl7bi 165 |
. . 3
⊢
(∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) → (𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → (𝐴 ∈ 𝐵 → 𝜓)))) |
16 | 15 | com34 83 |
. 2
⊢
(∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) → (𝐴 ∈ 𝐵 → (𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → 𝜓)))) |
17 | 16 | pm2.43d 50 |
1
⊢
(∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) → (𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → 𝜓))) |