| Step | Hyp | Ref
| Expression |
| 1 | | bj-gabima.nf |
. . . 4
⊢ (𝜑 → ∀𝑥𝜑) |
| 2 | | nfcvd 2906 |
. . . 4
⊢ (𝜑 → Ⅎ𝑥𝑦) |
| 3 | | vex 3484 |
. . . . 5
⊢ 𝑦 ∈ V |
| 4 | 3 | a1i 11 |
. . . 4
⊢ (𝜑 → 𝑦 ∈ V) |
| 5 | | df-rex 3071 |
. . . . . 6
⊢
(∃𝑧 ∈
{𝑥 ∣ 𝜓} (𝐹‘𝑧) = 𝑦 ↔ ∃𝑧(𝑧 ∈ {𝑥 ∣ 𝜓} ∧ (𝐹‘𝑧) = 𝑦)) |
| 6 | 5 | a1i 11 |
. . . . 5
⊢ (𝜑 → (∃𝑧 ∈ {𝑥 ∣ 𝜓} (𝐹‘𝑧) = 𝑦 ↔ ∃𝑧(𝑧 ∈ {𝑥 ∣ 𝜓} ∧ (𝐹‘𝑧) = 𝑦))) |
| 7 | | eqcom 2744 |
. . . . . . . 8
⊢ (𝑦 = (𝐹‘𝑧) ↔ (𝐹‘𝑧) = 𝑦) |
| 8 | | df-clab 2715 |
. . . . . . . . 9
⊢ (𝑧 ∈ {𝑥 ∣ 𝜓} ↔ [𝑧 / 𝑥]𝜓) |
| 9 | 8 | bicomi 224 |
. . . . . . . 8
⊢ ([𝑧 / 𝑥]𝜓 ↔ 𝑧 ∈ {𝑥 ∣ 𝜓}) |
| 10 | 7, 9 | anbi12ci 629 |
. . . . . . 7
⊢ ((𝑦 = (𝐹‘𝑧) ∧ [𝑧 / 𝑥]𝜓) ↔ (𝑧 ∈ {𝑥 ∣ 𝜓} ∧ (𝐹‘𝑧) = 𝑦)) |
| 11 | 10 | exbii 1848 |
. . . . . 6
⊢
(∃𝑧(𝑦 = (𝐹‘𝑧) ∧ [𝑧 / 𝑥]𝜓) ↔ ∃𝑧(𝑧 ∈ {𝑥 ∣ 𝜓} ∧ (𝐹‘𝑧) = 𝑦)) |
| 12 | 11 | a1i 11 |
. . . . 5
⊢ (𝜑 → (∃𝑧(𝑦 = (𝐹‘𝑧) ∧ [𝑧 / 𝑥]𝜓) ↔ ∃𝑧(𝑧 ∈ {𝑥 ∣ 𝜓} ∧ (𝐹‘𝑧) = 𝑦))) |
| 13 | 1 | nf5i 2146 |
. . . . . 6
⊢
Ⅎ𝑥𝜑 |
| 14 | | nfcv 2905 |
. . . . . . . . 9
⊢
Ⅎ𝑥𝑦 |
| 15 | 14 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → Ⅎ𝑥𝑦) |
| 16 | | bj-gabima.nff |
. . . . . . . . 9
⊢ (𝜑 → Ⅎ𝑥𝐹) |
| 17 | | nfcv 2905 |
. . . . . . . . . 10
⊢
Ⅎ𝑥𝑧 |
| 18 | 17 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → Ⅎ𝑥𝑧) |
| 19 | 16, 18 | nffvd 6918 |
. . . . . . . 8
⊢ (𝜑 → Ⅎ𝑥(𝐹‘𝑧)) |
| 20 | 15, 19 | nfeqd 2916 |
. . . . . . 7
⊢ (𝜑 → Ⅎ𝑥 𝑦 = (𝐹‘𝑧)) |
| 21 | | nfs1v 2156 |
. . . . . . . 8
⊢
Ⅎ𝑥[𝑧 / 𝑥]𝜓 |
| 22 | 21 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → Ⅎ𝑥[𝑧 / 𝑥]𝜓) |
| 23 | 20, 22 | nfand 1897 |
. . . . . 6
⊢ (𝜑 → Ⅎ𝑥(𝑦 = (𝐹‘𝑧) ∧ [𝑧 / 𝑥]𝜓)) |
| 24 | | fveq2 6906 |
. . . . . . . . 9
⊢ (𝑧 = 𝑥 → (𝐹‘𝑧) = (𝐹‘𝑥)) |
| 25 | 24 | eqeq2d 2748 |
. . . . . . . 8
⊢ (𝑧 = 𝑥 → (𝑦 = (𝐹‘𝑧) ↔ 𝑦 = (𝐹‘𝑥))) |
| 26 | | sbequ12r 2252 |
. . . . . . . 8
⊢ (𝑧 = 𝑥 → ([𝑧 / 𝑥]𝜓 ↔ 𝜓)) |
| 27 | 25, 26 | anbi12d 632 |
. . . . . . 7
⊢ (𝑧 = 𝑥 → ((𝑦 = (𝐹‘𝑧) ∧ [𝑧 / 𝑥]𝜓) ↔ (𝑦 = (𝐹‘𝑥) ∧ 𝜓))) |
| 28 | 27 | a1i 11 |
. . . . . 6
⊢ (𝜑 → (𝑧 = 𝑥 → ((𝑦 = (𝐹‘𝑧) ∧ [𝑧 / 𝑥]𝜓) ↔ (𝑦 = (𝐹‘𝑥) ∧ 𝜓)))) |
| 29 | 13, 23, 28 | cbvexdw 2341 |
. . . . 5
⊢ (𝜑 → (∃𝑧(𝑦 = (𝐹‘𝑧) ∧ [𝑧 / 𝑥]𝜓) ↔ ∃𝑥(𝑦 = (𝐹‘𝑥) ∧ 𝜓))) |
| 30 | 6, 12, 29 | 3bitr2rd 308 |
. . . 4
⊢ (𝜑 → (∃𝑥(𝑦 = (𝐹‘𝑥) ∧ 𝜓) ↔ ∃𝑧 ∈ {𝑥 ∣ 𝜓} (𝐹‘𝑧) = 𝑦)) |
| 31 | 1, 2, 4, 30 | bj-elgab 36940 |
. . 3
⊢ (𝜑 → (𝑦 ∈ {(𝐹‘𝑥) ∣ 𝑥 ∣ 𝜓} ↔ ∃𝑧 ∈ {𝑥 ∣ 𝜓} (𝐹‘𝑧) = 𝑦)) |
| 32 | | bj-gabima.fun |
. . . . 5
⊢ (𝜑 → Fun 𝐹) |
| 33 | 32 | funfnd 6597 |
. . . 4
⊢ (𝜑 → 𝐹 Fn dom 𝐹) |
| 34 | | bj-gabima.dm |
. . . 4
⊢ (𝜑 → {𝑥 ∣ 𝜓} ⊆ dom 𝐹) |
| 35 | 33, 34 | fvelimabd 6982 |
. . 3
⊢ (𝜑 → (𝑦 ∈ (𝐹 “ {𝑥 ∣ 𝜓}) ↔ ∃𝑧 ∈ {𝑥 ∣ 𝜓} (𝐹‘𝑧) = 𝑦)) |
| 36 | 31, 35 | bitr4d 282 |
. 2
⊢ (𝜑 → (𝑦 ∈ {(𝐹‘𝑥) ∣ 𝑥 ∣ 𝜓} ↔ 𝑦 ∈ (𝐹 “ {𝑥 ∣ 𝜓}))) |
| 37 | 36 | eqrdv 2735 |
1
⊢ (𝜑 → {(𝐹‘𝑥) ∣ 𝑥 ∣ 𝜓} = (𝐹 “ {𝑥 ∣ 𝜓})) |