Step |
Hyp |
Ref |
Expression |
1 |
|
bnj984.3 |
⊢ ( 𝜒 ↔ ( 𝑛 ∈ 𝐷 ∧ 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ) |
2 |
|
bnj984.11 |
⊢ 𝐵 = { 𝑓 ∣ ∃ 𝑛 ∈ 𝐷 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) } |
3 |
2
|
eleq2i |
⊢ ( 𝐺 ∈ 𝐵 ↔ 𝐺 ∈ { 𝑓 ∣ ∃ 𝑛 ∈ 𝐷 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) } ) |
4 |
|
sbc8g |
⊢ ( 𝐺 ∈ 𝐴 → ( [ 𝐺 / 𝑓 ] ∃ 𝑛 ∈ 𝐷 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ↔ 𝐺 ∈ { 𝑓 ∣ ∃ 𝑛 ∈ 𝐷 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) } ) ) |
5 |
3 4
|
bitr4id |
⊢ ( 𝐺 ∈ 𝐴 → ( 𝐺 ∈ 𝐵 ↔ [ 𝐺 / 𝑓 ] ∃ 𝑛 ∈ 𝐷 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ) ) |
6 |
|
df-rex |
⊢ ( ∃ 𝑛 ∈ 𝐷 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ↔ ∃ 𝑛 ( 𝑛 ∈ 𝐷 ∧ ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ) ) |
7 |
|
bnj252 |
⊢ ( ( 𝑛 ∈ 𝐷 ∧ 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ↔ ( 𝑛 ∈ 𝐷 ∧ ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ) ) |
8 |
1 7
|
bitri |
⊢ ( 𝜒 ↔ ( 𝑛 ∈ 𝐷 ∧ ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ) ) |
9 |
6 8
|
bnj133 |
⊢ ( ∃ 𝑛 ∈ 𝐷 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ↔ ∃ 𝑛 𝜒 ) |
10 |
9
|
sbcbii |
⊢ ( [ 𝐺 / 𝑓 ] ∃ 𝑛 ∈ 𝐷 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ↔ [ 𝐺 / 𝑓 ] ∃ 𝑛 𝜒 ) |
11 |
5 10
|
bitrdi |
⊢ ( 𝐺 ∈ 𝐴 → ( 𝐺 ∈ 𝐵 ↔ [ 𝐺 / 𝑓 ] ∃ 𝑛 𝜒 ) ) |