Step | Hyp | Ref
| Expression |
1 | | bnj976.4 |
. 2
⊢ (𝜒′ ↔ [𝐺 / 𝑓]𝜒) |
2 | | sbccow 3742 |
. 2
⊢
([𝐺 / ℎ][ℎ / 𝑓]𝜒 ↔ [𝐺 / 𝑓]𝜒) |
3 | | bnj976.5 |
. . 3
⊢ 𝐺 ∈ V |
4 | | bnj252 32661 |
. . . . . 6
⊢ ((𝑁 ∈ 𝐷 ∧ 𝑓 Fn 𝑁 ∧ 𝜑 ∧ 𝜓) ↔ (𝑁 ∈ 𝐷 ∧ (𝑓 Fn 𝑁 ∧ 𝜑 ∧ 𝜓))) |
5 | 4 | sbcbii 3780 |
. . . . 5
⊢
([ℎ / 𝑓](𝑁 ∈ 𝐷 ∧ 𝑓 Fn 𝑁 ∧ 𝜑 ∧ 𝜓) ↔ [ℎ / 𝑓](𝑁 ∈ 𝐷 ∧ (𝑓 Fn 𝑁 ∧ 𝜑 ∧ 𝜓))) |
6 | | bnj976.1 |
. . . . . 6
⊢ (𝜒 ↔ (𝑁 ∈ 𝐷 ∧ 𝑓 Fn 𝑁 ∧ 𝜑 ∧ 𝜓)) |
7 | 6 | sbcbii 3780 |
. . . . 5
⊢
([ℎ / 𝑓]𝜒 ↔ [ℎ / 𝑓](𝑁 ∈ 𝐷 ∧ 𝑓 Fn 𝑁 ∧ 𝜑 ∧ 𝜓)) |
8 | | vex 3434 |
. . . . . . . 8
⊢ ℎ ∈ V |
9 | 8 | bnj525 32697 |
. . . . . . 7
⊢
([ℎ / 𝑓]𝑁 ∈ 𝐷 ↔ 𝑁 ∈ 𝐷) |
10 | | sbc3an 3790 |
. . . . . . . 8
⊢
([ℎ / 𝑓](𝑓 Fn 𝑁 ∧ 𝜑 ∧ 𝜓) ↔ ([ℎ / 𝑓]𝑓 Fn 𝑁 ∧ [ℎ / 𝑓]𝜑 ∧ [ℎ / 𝑓]𝜓)) |
11 | | bnj62 32678 |
. . . . . . . . 9
⊢
([ℎ / 𝑓]𝑓 Fn 𝑁 ↔ ℎ Fn 𝑁) |
12 | 11 | 3anbi1i 1155 |
. . . . . . . 8
⊢
(([ℎ / 𝑓]𝑓 Fn 𝑁 ∧ [ℎ / 𝑓]𝜑 ∧ [ℎ / 𝑓]𝜓) ↔ (ℎ Fn 𝑁 ∧ [ℎ / 𝑓]𝜑 ∧ [ℎ / 𝑓]𝜓)) |
13 | 10, 12 | bitri 274 |
. . . . . . 7
⊢
([ℎ / 𝑓](𝑓 Fn 𝑁 ∧ 𝜑 ∧ 𝜓) ↔ (ℎ Fn 𝑁 ∧ [ℎ / 𝑓]𝜑 ∧ [ℎ / 𝑓]𝜓)) |
14 | 9, 13 | anbi12i 626 |
. . . . . 6
⊢
(([ℎ / 𝑓]𝑁 ∈ 𝐷 ∧ [ℎ / 𝑓](𝑓 Fn 𝑁 ∧ 𝜑 ∧ 𝜓)) ↔ (𝑁 ∈ 𝐷 ∧ (ℎ Fn 𝑁 ∧ [ℎ / 𝑓]𝜑 ∧ [ℎ / 𝑓]𝜓))) |
15 | | sbcan 3771 |
. . . . . 6
⊢
([ℎ / 𝑓](𝑁 ∈ 𝐷 ∧ (𝑓 Fn 𝑁 ∧ 𝜑 ∧ 𝜓)) ↔ ([ℎ / 𝑓]𝑁 ∈ 𝐷 ∧ [ℎ / 𝑓](𝑓 Fn 𝑁 ∧ 𝜑 ∧ 𝜓))) |
16 | | bnj252 32661 |
. . . . . 6
⊢ ((𝑁 ∈ 𝐷 ∧ ℎ Fn 𝑁 ∧ [ℎ / 𝑓]𝜑 ∧ [ℎ / 𝑓]𝜓) ↔ (𝑁 ∈ 𝐷 ∧ (ℎ Fn 𝑁 ∧ [ℎ / 𝑓]𝜑 ∧ [ℎ / 𝑓]𝜓))) |
17 | 14, 15, 16 | 3bitr4ri 303 |
. . . . 5
⊢ ((𝑁 ∈ 𝐷 ∧ ℎ Fn 𝑁 ∧ [ℎ / 𝑓]𝜑 ∧ [ℎ / 𝑓]𝜓) ↔ [ℎ / 𝑓](𝑁 ∈ 𝐷 ∧ (𝑓 Fn 𝑁 ∧ 𝜑 ∧ 𝜓))) |
18 | 5, 7, 17 | 3bitr4i 302 |
. . . 4
⊢
([ℎ / 𝑓]𝜒 ↔ (𝑁 ∈ 𝐷 ∧ ℎ Fn 𝑁 ∧ [ℎ / 𝑓]𝜑 ∧ [ℎ / 𝑓]𝜓)) |
19 | | fneq1 6520 |
. . . . . . 7
⊢ (ℎ = 𝐺 → (ℎ Fn 𝑁 ↔ 𝐺 Fn 𝑁)) |
20 | | sbceq1a 3730 |
. . . . . . . 8
⊢ (ℎ = 𝐺 → ([ℎ / 𝑓]𝜑 ↔ [𝐺 / ℎ][ℎ / 𝑓]𝜑)) |
21 | | bnj976.2 |
. . . . . . . . 9
⊢ (𝜑′ ↔ [𝐺 / 𝑓]𝜑) |
22 | | sbccow 3742 |
. . . . . . . . 9
⊢
([𝐺 / ℎ][ℎ / 𝑓]𝜑 ↔ [𝐺 / 𝑓]𝜑) |
23 | 21, 22 | bitr4i 277 |
. . . . . . . 8
⊢ (𝜑′ ↔ [𝐺 / ℎ][ℎ / 𝑓]𝜑) |
24 | 20, 23 | bitr4di 288 |
. . . . . . 7
⊢ (ℎ = 𝐺 → ([ℎ / 𝑓]𝜑 ↔ 𝜑′)) |
25 | | sbceq1a 3730 |
. . . . . . . 8
⊢ (ℎ = 𝐺 → ([ℎ / 𝑓]𝜓 ↔ [𝐺 / ℎ][ℎ / 𝑓]𝜓)) |
26 | | bnj976.3 |
. . . . . . . . 9
⊢ (𝜓′ ↔ [𝐺 / 𝑓]𝜓) |
27 | | sbccow 3742 |
. . . . . . . . 9
⊢
([𝐺 / ℎ][ℎ / 𝑓]𝜓 ↔ [𝐺 / 𝑓]𝜓) |
28 | 26, 27 | bitr4i 277 |
. . . . . . . 8
⊢ (𝜓′ ↔ [𝐺 / ℎ][ℎ / 𝑓]𝜓) |
29 | 25, 28 | bitr4di 288 |
. . . . . . 7
⊢ (ℎ = 𝐺 → ([ℎ / 𝑓]𝜓 ↔ 𝜓′)) |
30 | 19, 24, 29 | 3anbi123d 1434 |
. . . . . 6
⊢ (ℎ = 𝐺 → ((ℎ Fn 𝑁 ∧ [ℎ / 𝑓]𝜑 ∧ [ℎ / 𝑓]𝜓) ↔ (𝐺 Fn 𝑁 ∧ 𝜑′ ∧ 𝜓′))) |
31 | 30 | anbi2d 628 |
. . . . 5
⊢ (ℎ = 𝐺 → ((𝑁 ∈ 𝐷 ∧ (ℎ Fn 𝑁 ∧ [ℎ / 𝑓]𝜑 ∧ [ℎ / 𝑓]𝜓)) ↔ (𝑁 ∈ 𝐷 ∧ (𝐺 Fn 𝑁 ∧ 𝜑′ ∧ 𝜓′)))) |
32 | | bnj252 32661 |
. . . . 5
⊢ ((𝑁 ∈ 𝐷 ∧ 𝐺 Fn 𝑁 ∧ 𝜑′ ∧ 𝜓′) ↔ (𝑁 ∈ 𝐷 ∧ (𝐺 Fn 𝑁 ∧ 𝜑′ ∧ 𝜓′))) |
33 | 31, 16, 32 | 3bitr4g 313 |
. . . 4
⊢ (ℎ = 𝐺 → ((𝑁 ∈ 𝐷 ∧ ℎ Fn 𝑁 ∧ [ℎ / 𝑓]𝜑 ∧ [ℎ / 𝑓]𝜓) ↔ (𝑁 ∈ 𝐷 ∧ 𝐺 Fn 𝑁 ∧ 𝜑′ ∧ 𝜓′))) |
34 | 18, 33 | syl5bb 282 |
. . 3
⊢ (ℎ = 𝐺 → ([ℎ / 𝑓]𝜒 ↔ (𝑁 ∈ 𝐷 ∧ 𝐺 Fn 𝑁 ∧ 𝜑′ ∧ 𝜓′))) |
35 | 3, 34 | sbcie 3762 |
. 2
⊢
([𝐺 / ℎ][ℎ / 𝑓]𝜒 ↔ (𝑁 ∈ 𝐷 ∧ 𝐺 Fn 𝑁 ∧ 𝜑′ ∧ 𝜓′)) |
36 | 1, 2, 35 | 3bitr2i 298 |
1
⊢ (𝜒′ ↔ (𝑁 ∈ 𝐷 ∧ 𝐺 Fn 𝑁 ∧ 𝜑′ ∧ 𝜓′)) |