Proof of Theorem ralxpxfr2d
Step | Hyp | Ref
| Expression |
1 | | df-ral 2901 |
. . . 4
⊢
(∀𝑥 ∈
𝐵 𝜓 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝜓)) |
2 | | ralxpxfr2d.b |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ 𝐵 ↔ ∃𝑦 ∈ 𝐶 ∃𝑧 ∈ 𝐷 𝑥 = 𝐴)) |
3 | 2 | imbi1d 330 |
. . . . 5
⊢ (𝜑 → ((𝑥 ∈ 𝐵 → 𝜓) ↔ (∃𝑦 ∈ 𝐶 ∃𝑧 ∈ 𝐷 𝑥 = 𝐴 → 𝜓))) |
4 | 3 | albidv 1836 |
. . . 4
⊢ (𝜑 → (∀𝑥(𝑥 ∈ 𝐵 → 𝜓) ↔ ∀𝑥(∃𝑦 ∈ 𝐶 ∃𝑧 ∈ 𝐷 𝑥 = 𝐴 → 𝜓))) |
5 | 1, 4 | syl5bb 271 |
. . 3
⊢ (𝜑 → (∀𝑥 ∈ 𝐵 𝜓 ↔ ∀𝑥(∃𝑦 ∈ 𝐶 ∃𝑧 ∈ 𝐷 𝑥 = 𝐴 → 𝜓))) |
6 | | ralcom4 3197 |
. . . 4
⊢
(∀𝑦 ∈
𝐶 ∀𝑥∀𝑧 ∈ 𝐷 (𝑥 = 𝐴 → 𝜓) ↔ ∀𝑥∀𝑦 ∈ 𝐶 ∀𝑧 ∈ 𝐷 (𝑥 = 𝐴 → 𝜓)) |
7 | | ralcom4 3197 |
. . . . 5
⊢
(∀𝑧 ∈
𝐷 ∀𝑥(𝑥 = 𝐴 → 𝜓) ↔ ∀𝑥∀𝑧 ∈ 𝐷 (𝑥 = 𝐴 → 𝜓)) |
8 | 7 | ralbii 2963 |
. . . 4
⊢
(∀𝑦 ∈
𝐶 ∀𝑧 ∈ 𝐷 ∀𝑥(𝑥 = 𝐴 → 𝜓) ↔ ∀𝑦 ∈ 𝐶 ∀𝑥∀𝑧 ∈ 𝐷 (𝑥 = 𝐴 → 𝜓)) |
9 | | r19.23v 3005 |
. . . . . . 7
⊢
(∀𝑧 ∈
𝐷 (𝑥 = 𝐴 → 𝜓) ↔ (∃𝑧 ∈ 𝐷 𝑥 = 𝐴 → 𝜓)) |
10 | 9 | ralbii 2963 |
. . . . . 6
⊢
(∀𝑦 ∈
𝐶 ∀𝑧 ∈ 𝐷 (𝑥 = 𝐴 → 𝜓) ↔ ∀𝑦 ∈ 𝐶 (∃𝑧 ∈ 𝐷 𝑥 = 𝐴 → 𝜓)) |
11 | | r19.23v 3005 |
. . . . . 6
⊢
(∀𝑦 ∈
𝐶 (∃𝑧 ∈ 𝐷 𝑥 = 𝐴 → 𝜓) ↔ (∃𝑦 ∈ 𝐶 ∃𝑧 ∈ 𝐷 𝑥 = 𝐴 → 𝜓)) |
12 | 10, 11 | bitr2i 264 |
. . . . 5
⊢
((∃𝑦 ∈
𝐶 ∃𝑧 ∈ 𝐷 𝑥 = 𝐴 → 𝜓) ↔ ∀𝑦 ∈ 𝐶 ∀𝑧 ∈ 𝐷 (𝑥 = 𝐴 → 𝜓)) |
13 | 12 | albii 1737 |
. . . 4
⊢
(∀𝑥(∃𝑦 ∈ 𝐶 ∃𝑧 ∈ 𝐷 𝑥 = 𝐴 → 𝜓) ↔ ∀𝑥∀𝑦 ∈ 𝐶 ∀𝑧 ∈ 𝐷 (𝑥 = 𝐴 → 𝜓)) |
14 | 6, 8, 13 | 3bitr4ri 292 |
. . 3
⊢
(∀𝑥(∃𝑦 ∈ 𝐶 ∃𝑧 ∈ 𝐷 𝑥 = 𝐴 → 𝜓) ↔ ∀𝑦 ∈ 𝐶 ∀𝑧 ∈ 𝐷 ∀𝑥(𝑥 = 𝐴 → 𝜓)) |
15 | 5, 14 | syl6bb 275 |
. 2
⊢ (𝜑 → (∀𝑥 ∈ 𝐵 𝜓 ↔ ∀𝑦 ∈ 𝐶 ∀𝑧 ∈ 𝐷 ∀𝑥(𝑥 = 𝐴 → 𝜓))) |
16 | | ralxpxfr2d.c |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 ↔ 𝜒)) |
17 | 16 | pm5.74da 719 |
. . . . 5
⊢ (𝜑 → ((𝑥 = 𝐴 → 𝜓) ↔ (𝑥 = 𝐴 → 𝜒))) |
18 | 17 | albidv 1836 |
. . . 4
⊢ (𝜑 → (∀𝑥(𝑥 = 𝐴 → 𝜓) ↔ ∀𝑥(𝑥 = 𝐴 → 𝜒))) |
19 | | ralxpxfr2d.a |
. . . . 5
⊢ 𝐴 ∈ V |
20 | | biidd 251 |
. . . . 5
⊢ (𝑥 = 𝐴 → (𝜒 ↔ 𝜒)) |
21 | 19, 20 | ceqsalv 3206 |
. . . 4
⊢
(∀𝑥(𝑥 = 𝐴 → 𝜒) ↔ 𝜒) |
22 | 18, 21 | syl6bb 275 |
. . 3
⊢ (𝜑 → (∀𝑥(𝑥 = 𝐴 → 𝜓) ↔ 𝜒)) |
23 | 22 | 2ralbidv 2972 |
. 2
⊢ (𝜑 → (∀𝑦 ∈ 𝐶 ∀𝑧 ∈ 𝐷 ∀𝑥(𝑥 = 𝐴 → 𝜓) ↔ ∀𝑦 ∈ 𝐶 ∀𝑧 ∈ 𝐷 𝜒)) |
24 | 15, 23 | bitrd 267 |
1
⊢ (𝜑 → (∀𝑥 ∈ 𝐵 𝜓 ↔ ∀𝑦 ∈ 𝐶 ∀𝑧 ∈ 𝐷 𝜒)) |