Step |
Hyp |
Ref |
Expression |
1 |
|
bnj976.1 |
⊢ ( 𝜒 ↔ ( 𝑁 ∈ 𝐷 ∧ 𝑓 Fn 𝑁 ∧ 𝜑 ∧ 𝜓 ) ) |
2 |
|
bnj976.2 |
⊢ ( 𝜑′ ↔ [ 𝐺 / 𝑓 ] 𝜑 ) |
3 |
|
bnj976.3 |
⊢ ( 𝜓′ ↔ [ 𝐺 / 𝑓 ] 𝜓 ) |
4 |
|
bnj976.4 |
⊢ ( 𝜒′ ↔ [ 𝐺 / 𝑓 ] 𝜒 ) |
5 |
|
bnj976.5 |
⊢ 𝐺 ∈ V |
6 |
|
sbccow |
⊢ ( [ 𝐺 / ℎ ] [ ℎ / 𝑓 ] 𝜒 ↔ [ 𝐺 / 𝑓 ] 𝜒 ) |
7 |
|
bnj252 |
⊢ ( ( 𝑁 ∈ 𝐷 ∧ 𝑓 Fn 𝑁 ∧ 𝜑 ∧ 𝜓 ) ↔ ( 𝑁 ∈ 𝐷 ∧ ( 𝑓 Fn 𝑁 ∧ 𝜑 ∧ 𝜓 ) ) ) |
8 |
7
|
sbcbii |
⊢ ( [ ℎ / 𝑓 ] ( 𝑁 ∈ 𝐷 ∧ 𝑓 Fn 𝑁 ∧ 𝜑 ∧ 𝜓 ) ↔ [ ℎ / 𝑓 ] ( 𝑁 ∈ 𝐷 ∧ ( 𝑓 Fn 𝑁 ∧ 𝜑 ∧ 𝜓 ) ) ) |
9 |
1
|
sbcbii |
⊢ ( [ ℎ / 𝑓 ] 𝜒 ↔ [ ℎ / 𝑓 ] ( 𝑁 ∈ 𝐷 ∧ 𝑓 Fn 𝑁 ∧ 𝜑 ∧ 𝜓 ) ) |
10 |
|
vex |
⊢ ℎ ∈ V |
11 |
10
|
bnj525 |
⊢ ( [ ℎ / 𝑓 ] 𝑁 ∈ 𝐷 ↔ 𝑁 ∈ 𝐷 ) |
12 |
|
sbc3an |
⊢ ( [ ℎ / 𝑓 ] ( 𝑓 Fn 𝑁 ∧ 𝜑 ∧ 𝜓 ) ↔ ( [ ℎ / 𝑓 ] 𝑓 Fn 𝑁 ∧ [ ℎ / 𝑓 ] 𝜑 ∧ [ ℎ / 𝑓 ] 𝜓 ) ) |
13 |
|
bnj62 |
⊢ ( [ ℎ / 𝑓 ] 𝑓 Fn 𝑁 ↔ ℎ Fn 𝑁 ) |
14 |
13
|
3anbi1i |
⊢ ( ( [ ℎ / 𝑓 ] 𝑓 Fn 𝑁 ∧ [ ℎ / 𝑓 ] 𝜑 ∧ [ ℎ / 𝑓 ] 𝜓 ) ↔ ( ℎ Fn 𝑁 ∧ [ ℎ / 𝑓 ] 𝜑 ∧ [ ℎ / 𝑓 ] 𝜓 ) ) |
15 |
12 14
|
bitri |
⊢ ( [ ℎ / 𝑓 ] ( 𝑓 Fn 𝑁 ∧ 𝜑 ∧ 𝜓 ) ↔ ( ℎ Fn 𝑁 ∧ [ ℎ / 𝑓 ] 𝜑 ∧ [ ℎ / 𝑓 ] 𝜓 ) ) |
16 |
11 15
|
anbi12i |
⊢ ( ( [ ℎ / 𝑓 ] 𝑁 ∈ 𝐷 ∧ [ ℎ / 𝑓 ] ( 𝑓 Fn 𝑁 ∧ 𝜑 ∧ 𝜓 ) ) ↔ ( 𝑁 ∈ 𝐷 ∧ ( ℎ Fn 𝑁 ∧ [ ℎ / 𝑓 ] 𝜑 ∧ [ ℎ / 𝑓 ] 𝜓 ) ) ) |
17 |
|
sbcan |
⊢ ( [ ℎ / 𝑓 ] ( 𝑁 ∈ 𝐷 ∧ ( 𝑓 Fn 𝑁 ∧ 𝜑 ∧ 𝜓 ) ) ↔ ( [ ℎ / 𝑓 ] 𝑁 ∈ 𝐷 ∧ [ ℎ / 𝑓 ] ( 𝑓 Fn 𝑁 ∧ 𝜑 ∧ 𝜓 ) ) ) |
18 |
|
bnj252 |
⊢ ( ( 𝑁 ∈ 𝐷 ∧ ℎ Fn 𝑁 ∧ [ ℎ / 𝑓 ] 𝜑 ∧ [ ℎ / 𝑓 ] 𝜓 ) ↔ ( 𝑁 ∈ 𝐷 ∧ ( ℎ Fn 𝑁 ∧ [ ℎ / 𝑓 ] 𝜑 ∧ [ ℎ / 𝑓 ] 𝜓 ) ) ) |
19 |
16 17 18
|
3bitr4ri |
⊢ ( ( 𝑁 ∈ 𝐷 ∧ ℎ Fn 𝑁 ∧ [ ℎ / 𝑓 ] 𝜑 ∧ [ ℎ / 𝑓 ] 𝜓 ) ↔ [ ℎ / 𝑓 ] ( 𝑁 ∈ 𝐷 ∧ ( 𝑓 Fn 𝑁 ∧ 𝜑 ∧ 𝜓 ) ) ) |
20 |
8 9 19
|
3bitr4i |
⊢ ( [ ℎ / 𝑓 ] 𝜒 ↔ ( 𝑁 ∈ 𝐷 ∧ ℎ Fn 𝑁 ∧ [ ℎ / 𝑓 ] 𝜑 ∧ [ ℎ / 𝑓 ] 𝜓 ) ) |
21 |
|
fneq1 |
⊢ ( ℎ = 𝐺 → ( ℎ Fn 𝑁 ↔ 𝐺 Fn 𝑁 ) ) |
22 |
|
sbceq1a |
⊢ ( ℎ = 𝐺 → ( [ ℎ / 𝑓 ] 𝜑 ↔ [ 𝐺 / ℎ ] [ ℎ / 𝑓 ] 𝜑 ) ) |
23 |
|
sbccow |
⊢ ( [ 𝐺 / ℎ ] [ ℎ / 𝑓 ] 𝜑 ↔ [ 𝐺 / 𝑓 ] 𝜑 ) |
24 |
2 23
|
bitr4i |
⊢ ( 𝜑′ ↔ [ 𝐺 / ℎ ] [ ℎ / 𝑓 ] 𝜑 ) |
25 |
22 24
|
bitr4di |
⊢ ( ℎ = 𝐺 → ( [ ℎ / 𝑓 ] 𝜑 ↔ 𝜑′ ) ) |
26 |
|
sbceq1a |
⊢ ( ℎ = 𝐺 → ( [ ℎ / 𝑓 ] 𝜓 ↔ [ 𝐺 / ℎ ] [ ℎ / 𝑓 ] 𝜓 ) ) |
27 |
|
sbccow |
⊢ ( [ 𝐺 / ℎ ] [ ℎ / 𝑓 ] 𝜓 ↔ [ 𝐺 / 𝑓 ] 𝜓 ) |
28 |
3 27
|
bitr4i |
⊢ ( 𝜓′ ↔ [ 𝐺 / ℎ ] [ ℎ / 𝑓 ] 𝜓 ) |
29 |
26 28
|
bitr4di |
⊢ ( ℎ = 𝐺 → ( [ ℎ / 𝑓 ] 𝜓 ↔ 𝜓′ ) ) |
30 |
21 25 29
|
3anbi123d |
⊢ ( ℎ = 𝐺 → ( ( ℎ Fn 𝑁 ∧ [ ℎ / 𝑓 ] 𝜑 ∧ [ ℎ / 𝑓 ] 𝜓 ) ↔ ( 𝐺 Fn 𝑁 ∧ 𝜑′ ∧ 𝜓′ ) ) ) |
31 |
30
|
anbi2d |
⊢ ( ℎ = 𝐺 → ( ( 𝑁 ∈ 𝐷 ∧ ( ℎ Fn 𝑁 ∧ [ ℎ / 𝑓 ] 𝜑 ∧ [ ℎ / 𝑓 ] 𝜓 ) ) ↔ ( 𝑁 ∈ 𝐷 ∧ ( 𝐺 Fn 𝑁 ∧ 𝜑′ ∧ 𝜓′ ) ) ) ) |
32 |
|
bnj252 |
⊢ ( ( 𝑁 ∈ 𝐷 ∧ 𝐺 Fn 𝑁 ∧ 𝜑′ ∧ 𝜓′ ) ↔ ( 𝑁 ∈ 𝐷 ∧ ( 𝐺 Fn 𝑁 ∧ 𝜑′ ∧ 𝜓′ ) ) ) |
33 |
31 18 32
|
3bitr4g |
⊢ ( ℎ = 𝐺 → ( ( 𝑁 ∈ 𝐷 ∧ ℎ Fn 𝑁 ∧ [ ℎ / 𝑓 ] 𝜑 ∧ [ ℎ / 𝑓 ] 𝜓 ) ↔ ( 𝑁 ∈ 𝐷 ∧ 𝐺 Fn 𝑁 ∧ 𝜑′ ∧ 𝜓′ ) ) ) |
34 |
20 33
|
syl5bb |
⊢ ( ℎ = 𝐺 → ( [ ℎ / 𝑓 ] 𝜒 ↔ ( 𝑁 ∈ 𝐷 ∧ 𝐺 Fn 𝑁 ∧ 𝜑′ ∧ 𝜓′ ) ) ) |
35 |
5 34
|
sbcie |
⊢ ( [ 𝐺 / ℎ ] [ ℎ / 𝑓 ] 𝜒 ↔ ( 𝑁 ∈ 𝐷 ∧ 𝐺 Fn 𝑁 ∧ 𝜑′ ∧ 𝜓′ ) ) |
36 |
4 6 35
|
3bitr2i |
⊢ ( 𝜒′ ↔ ( 𝑁 ∈ 𝐷 ∧ 𝐺 Fn 𝑁 ∧ 𝜑′ ∧ 𝜓′ ) ) |