| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | bnj976.4 | . 2
⊢ (𝜒′ ↔ [𝐺 / 𝑓]𝜒) | 
| 2 |  | sbccow 3810 | . 2
⊢
([𝐺 / ℎ][ℎ / 𝑓]𝜒 ↔ [𝐺 / 𝑓]𝜒) | 
| 3 |  | bnj976.5 | . . 3
⊢ 𝐺 ∈ V | 
| 4 |  | bnj252 34718 | . . . . . 6
⊢ ((𝑁 ∈ 𝐷 ∧ 𝑓 Fn 𝑁 ∧ 𝜑 ∧ 𝜓) ↔ (𝑁 ∈ 𝐷 ∧ (𝑓 Fn 𝑁 ∧ 𝜑 ∧ 𝜓))) | 
| 5 | 4 | sbcbii 3845 | . . . . 5
⊢
([ℎ / 𝑓](𝑁 ∈ 𝐷 ∧ 𝑓 Fn 𝑁 ∧ 𝜑 ∧ 𝜓) ↔ [ℎ / 𝑓](𝑁 ∈ 𝐷 ∧ (𝑓 Fn 𝑁 ∧ 𝜑 ∧ 𝜓))) | 
| 6 |  | bnj976.1 | . . . . . 6
⊢ (𝜒 ↔ (𝑁 ∈ 𝐷 ∧ 𝑓 Fn 𝑁 ∧ 𝜑 ∧ 𝜓)) | 
| 7 | 6 | sbcbii 3845 | . . . . 5
⊢
([ℎ / 𝑓]𝜒 ↔ [ℎ / 𝑓](𝑁 ∈ 𝐷 ∧ 𝑓 Fn 𝑁 ∧ 𝜑 ∧ 𝜓)) | 
| 8 |  | vex 3483 | . . . . . . . 8
⊢ ℎ ∈ V | 
| 9 | 8 | bnj525 34753 | . . . . . . 7
⊢
([ℎ / 𝑓]𝑁 ∈ 𝐷 ↔ 𝑁 ∈ 𝐷) | 
| 10 |  | sbc3an 3854 | . . . . . . . 8
⊢
([ℎ / 𝑓](𝑓 Fn 𝑁 ∧ 𝜑 ∧ 𝜓) ↔ ([ℎ / 𝑓]𝑓 Fn 𝑁 ∧ [ℎ / 𝑓]𝜑 ∧ [ℎ / 𝑓]𝜓)) | 
| 11 |  | bnj62 34735 | . . . . . . . . 9
⊢
([ℎ / 𝑓]𝑓 Fn 𝑁 ↔ ℎ Fn 𝑁) | 
| 12 | 11 | 3anbi1i 1157 | . . . . . . . 8
⊢
(([ℎ / 𝑓]𝑓 Fn 𝑁 ∧ [ℎ / 𝑓]𝜑 ∧ [ℎ / 𝑓]𝜓) ↔ (ℎ Fn 𝑁 ∧ [ℎ / 𝑓]𝜑 ∧ [ℎ / 𝑓]𝜓)) | 
| 13 | 10, 12 | bitri 275 | . . . . . . 7
⊢
([ℎ / 𝑓](𝑓 Fn 𝑁 ∧ 𝜑 ∧ 𝜓) ↔ (ℎ Fn 𝑁 ∧ [ℎ / 𝑓]𝜑 ∧ [ℎ / 𝑓]𝜓)) | 
| 14 | 9, 13 | anbi12i 628 | . . . . . 6
⊢
(([ℎ / 𝑓]𝑁 ∈ 𝐷 ∧ [ℎ / 𝑓](𝑓 Fn 𝑁 ∧ 𝜑 ∧ 𝜓)) ↔ (𝑁 ∈ 𝐷 ∧ (ℎ Fn 𝑁 ∧ [ℎ / 𝑓]𝜑 ∧ [ℎ / 𝑓]𝜓))) | 
| 15 |  | sbcan 3837 | . . . . . 6
⊢
([ℎ / 𝑓](𝑁 ∈ 𝐷 ∧ (𝑓 Fn 𝑁 ∧ 𝜑 ∧ 𝜓)) ↔ ([ℎ / 𝑓]𝑁 ∈ 𝐷 ∧ [ℎ / 𝑓](𝑓 Fn 𝑁 ∧ 𝜑 ∧ 𝜓))) | 
| 16 |  | bnj252 34718 | . . . . . 6
⊢ ((𝑁 ∈ 𝐷 ∧ ℎ Fn 𝑁 ∧ [ℎ / 𝑓]𝜑 ∧ [ℎ / 𝑓]𝜓) ↔ (𝑁 ∈ 𝐷 ∧ (ℎ Fn 𝑁 ∧ [ℎ / 𝑓]𝜑 ∧ [ℎ / 𝑓]𝜓))) | 
| 17 | 14, 15, 16 | 3bitr4ri 304 | . . . . 5
⊢ ((𝑁 ∈ 𝐷 ∧ ℎ Fn 𝑁 ∧ [ℎ / 𝑓]𝜑 ∧ [ℎ / 𝑓]𝜓) ↔ [ℎ / 𝑓](𝑁 ∈ 𝐷 ∧ (𝑓 Fn 𝑁 ∧ 𝜑 ∧ 𝜓))) | 
| 18 | 5, 7, 17 | 3bitr4i 303 | . . . 4
⊢
([ℎ / 𝑓]𝜒 ↔ (𝑁 ∈ 𝐷 ∧ ℎ Fn 𝑁 ∧ [ℎ / 𝑓]𝜑 ∧ [ℎ / 𝑓]𝜓)) | 
| 19 |  | fneq1 6658 | . . . . . . 7
⊢ (ℎ = 𝐺 → (ℎ Fn 𝑁 ↔ 𝐺 Fn 𝑁)) | 
| 20 |  | sbceq1a 3798 | . . . . . . . 8
⊢ (ℎ = 𝐺 → ([ℎ / 𝑓]𝜑 ↔ [𝐺 / ℎ][ℎ / 𝑓]𝜑)) | 
| 21 |  | bnj976.2 | . . . . . . . . 9
⊢ (𝜑′ ↔ [𝐺 / 𝑓]𝜑) | 
| 22 |  | sbccow 3810 | . . . . . . . . 9
⊢
([𝐺 / ℎ][ℎ / 𝑓]𝜑 ↔ [𝐺 / 𝑓]𝜑) | 
| 23 | 21, 22 | bitr4i 278 | . . . . . . . 8
⊢ (𝜑′ ↔ [𝐺 / ℎ][ℎ / 𝑓]𝜑) | 
| 24 | 20, 23 | bitr4di 289 | . . . . . . 7
⊢ (ℎ = 𝐺 → ([ℎ / 𝑓]𝜑 ↔ 𝜑′)) | 
| 25 |  | sbceq1a 3798 | . . . . . . . 8
⊢ (ℎ = 𝐺 → ([ℎ / 𝑓]𝜓 ↔ [𝐺 / ℎ][ℎ / 𝑓]𝜓)) | 
| 26 |  | bnj976.3 | . . . . . . . . 9
⊢ (𝜓′ ↔ [𝐺 / 𝑓]𝜓) | 
| 27 |  | sbccow 3810 | . . . . . . . . 9
⊢
([𝐺 / ℎ][ℎ / 𝑓]𝜓 ↔ [𝐺 / 𝑓]𝜓) | 
| 28 | 26, 27 | bitr4i 278 | . . . . . . . 8
⊢ (𝜓′ ↔ [𝐺 / ℎ][ℎ / 𝑓]𝜓) | 
| 29 | 25, 28 | bitr4di 289 | . . . . . . 7
⊢ (ℎ = 𝐺 → ([ℎ / 𝑓]𝜓 ↔ 𝜓′)) | 
| 30 | 19, 24, 29 | 3anbi123d 1437 | . . . . . 6
⊢ (ℎ = 𝐺 → ((ℎ Fn 𝑁 ∧ [ℎ / 𝑓]𝜑 ∧ [ℎ / 𝑓]𝜓) ↔ (𝐺 Fn 𝑁 ∧ 𝜑′ ∧ 𝜓′))) | 
| 31 | 30 | anbi2d 630 | . . . . 5
⊢ (ℎ = 𝐺 → ((𝑁 ∈ 𝐷 ∧ (ℎ Fn 𝑁 ∧ [ℎ / 𝑓]𝜑 ∧ [ℎ / 𝑓]𝜓)) ↔ (𝑁 ∈ 𝐷 ∧ (𝐺 Fn 𝑁 ∧ 𝜑′ ∧ 𝜓′)))) | 
| 32 |  | bnj252 34718 | . . . . 5
⊢ ((𝑁 ∈ 𝐷 ∧ 𝐺 Fn 𝑁 ∧ 𝜑′ ∧ 𝜓′) ↔ (𝑁 ∈ 𝐷 ∧ (𝐺 Fn 𝑁 ∧ 𝜑′ ∧ 𝜓′))) | 
| 33 | 31, 16, 32 | 3bitr4g 314 | . . . 4
⊢ (ℎ = 𝐺 → ((𝑁 ∈ 𝐷 ∧ ℎ Fn 𝑁 ∧ [ℎ / 𝑓]𝜑 ∧ [ℎ / 𝑓]𝜓) ↔ (𝑁 ∈ 𝐷 ∧ 𝐺 Fn 𝑁 ∧ 𝜑′ ∧ 𝜓′))) | 
| 34 | 18, 33 | bitrid 283 | . . 3
⊢ (ℎ = 𝐺 → ([ℎ / 𝑓]𝜒 ↔ (𝑁 ∈ 𝐷 ∧ 𝐺 Fn 𝑁 ∧ 𝜑′ ∧ 𝜓′))) | 
| 35 | 3, 34 | sbcie 3829 | . 2
⊢
([𝐺 / ℎ][ℎ / 𝑓]𝜒 ↔ (𝑁 ∈ 𝐷 ∧ 𝐺 Fn 𝑁 ∧ 𝜑′ ∧ 𝜓′)) | 
| 36 | 1, 2, 35 | 3bitr2i 299 | 1
⊢ (𝜒′ ↔ (𝑁 ∈ 𝐷 ∧ 𝐺 Fn 𝑁 ∧ 𝜑′ ∧ 𝜓′)) |