Step |
Hyp |
Ref |
Expression |
1 |
|
bnj985v.3 |
⊢ ( 𝜒 ↔ ( 𝑛 ∈ 𝐷 ∧ 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ) |
2 |
|
bnj985v.6 |
⊢ ( 𝜒′ ↔ [ 𝑝 / 𝑛 ] 𝜒 ) |
3 |
|
bnj985v.9 |
⊢ ( 𝜒″ ↔ [ 𝐺 / 𝑓 ] 𝜒′ ) |
4 |
|
bnj985v.11 |
⊢ 𝐵 = { 𝑓 ∣ ∃ 𝑛 ∈ 𝐷 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) } |
5 |
|
bnj985v.13 |
⊢ 𝐺 = ( 𝑓 ∪ { 〈 𝑛 , 𝐶 〉 } ) |
6 |
5
|
bnj918 |
⊢ 𝐺 ∈ V |
7 |
1 4
|
bnj984 |
⊢ ( 𝐺 ∈ V → ( 𝐺 ∈ 𝐵 ↔ [ 𝐺 / 𝑓 ] ∃ 𝑛 𝜒 ) ) |
8 |
6 7
|
ax-mp |
⊢ ( 𝐺 ∈ 𝐵 ↔ [ 𝐺 / 𝑓 ] ∃ 𝑛 𝜒 ) |
9 |
|
sbcex2 |
⊢ ( [ 𝐺 / 𝑓 ] ∃ 𝑝 𝜒′ ↔ ∃ 𝑝 [ 𝐺 / 𝑓 ] 𝜒′ ) |
10 |
|
nfv |
⊢ Ⅎ 𝑝 𝜒 |
11 |
10
|
sb8ev |
⊢ ( ∃ 𝑛 𝜒 ↔ ∃ 𝑝 [ 𝑝 / 𝑛 ] 𝜒 ) |
12 |
|
sbsbc |
⊢ ( [ 𝑝 / 𝑛 ] 𝜒 ↔ [ 𝑝 / 𝑛 ] 𝜒 ) |
13 |
12
|
exbii |
⊢ ( ∃ 𝑝 [ 𝑝 / 𝑛 ] 𝜒 ↔ ∃ 𝑝 [ 𝑝 / 𝑛 ] 𝜒 ) |
14 |
11 13
|
bitri |
⊢ ( ∃ 𝑛 𝜒 ↔ ∃ 𝑝 [ 𝑝 / 𝑛 ] 𝜒 ) |
15 |
14 2
|
bnj133 |
⊢ ( ∃ 𝑛 𝜒 ↔ ∃ 𝑝 𝜒′ ) |
16 |
15
|
sbcbii |
⊢ ( [ 𝐺 / 𝑓 ] ∃ 𝑛 𝜒 ↔ [ 𝐺 / 𝑓 ] ∃ 𝑝 𝜒′ ) |
17 |
3
|
exbii |
⊢ ( ∃ 𝑝 𝜒″ ↔ ∃ 𝑝 [ 𝐺 / 𝑓 ] 𝜒′ ) |
18 |
9 16 17
|
3bitr4i |
⊢ ( [ 𝐺 / 𝑓 ] ∃ 𝑛 𝜒 ↔ ∃ 𝑝 𝜒″ ) |
19 |
8 18
|
bitri |
⊢ ( 𝐺 ∈ 𝐵 ↔ ∃ 𝑝 𝜒″ ) |