Step |
Hyp |
Ref |
Expression |
1 |
|
sneq |
⊢ ( 𝑥 = 𝐴 → { 𝑥 } = { 𝐴 } ) |
2 |
1
|
reseq2d |
⊢ ( 𝑥 = 𝐴 → ( 𝐹 ↾ { 𝑥 } ) = ( 𝐹 ↾ { 𝐴 } ) ) |
3 |
2
|
funeqd |
⊢ ( 𝑥 = 𝐴 → ( Fun ( 𝐹 ↾ { 𝑥 } ) ↔ Fun ( 𝐹 ↾ { 𝐴 } ) ) ) |
4 |
|
breq1 |
⊢ ( 𝑥 = 𝐴 → ( 𝑥 𝐹 𝑦 ↔ 𝐴 𝐹 𝑦 ) ) |
5 |
4
|
mobidv |
⊢ ( 𝑥 = 𝐴 → ( ∃* 𝑦 𝑥 𝐹 𝑦 ↔ ∃* 𝑦 𝐴 𝐹 𝑦 ) ) |
6 |
3 5
|
imbi12d |
⊢ ( 𝑥 = 𝐴 → ( ( Fun ( 𝐹 ↾ { 𝑥 } ) → ∃* 𝑦 𝑥 𝐹 𝑦 ) ↔ ( Fun ( 𝐹 ↾ { 𝐴 } ) → ∃* 𝑦 𝐴 𝐹 𝑦 ) ) ) |
7 |
|
funressnvmo |
⊢ ( Fun ( 𝐹 ↾ { 𝑥 } ) → ∃* 𝑦 𝑥 𝐹 𝑦 ) |
8 |
6 7
|
vtoclg |
⊢ ( 𝐴 ∈ 𝑉 → ( Fun ( 𝐹 ↾ { 𝐴 } ) → ∃* 𝑦 𝐴 𝐹 𝑦 ) ) |
9 |
8
|
imp |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ Fun ( 𝐹 ↾ { 𝐴 } ) ) → ∃* 𝑦 𝐴 𝐹 𝑦 ) |