Step | Hyp | Ref
| Expression |
1 | | vex 2715 |
. . . 4
⊢ 𝑥 ∈ V |
2 | | id 19 |
. . . . . . 7
⊢ (𝑥 = 𝑧 → 𝑥 = 𝑧) |
3 | | csbeq1a 3040 |
. . . . . . 7
⊢ (𝑥 = 𝑧 → 𝐴 = ⦋𝑧 / 𝑥⦌𝐴) |
4 | 2, 3 | eleq12d 2228 |
. . . . . 6
⊢ (𝑥 = 𝑧 → (𝑥 ∈ 𝐴 ↔ 𝑧 ∈ ⦋𝑧 / 𝑥⦌𝐴)) |
5 | | csbeq1a 3040 |
. . . . . . 7
⊢ (𝑥 = 𝑧 → 𝐵 = ⦋𝑧 / 𝑥⦌𝐵) |
6 | 5 | biantrud 302 |
. . . . . 6
⊢ (𝑥 = 𝑧 → (𝑧 ∈ ⦋𝑧 / 𝑥⦌𝐴 ↔ (𝑧 ∈ ⦋𝑧 / 𝑥⦌𝐴 ∧ 𝐵 = ⦋𝑧 / 𝑥⦌𝐵))) |
7 | 4, 6 | bitr2d 188 |
. . . . 5
⊢ (𝑥 = 𝑧 → ((𝑧 ∈ ⦋𝑧 / 𝑥⦌𝐴 ∧ 𝐵 = ⦋𝑧 / 𝑥⦌𝐵) ↔ 𝑥 ∈ 𝐴)) |
8 | 7 | equcoms 1688 |
. . . 4
⊢ (𝑧 = 𝑥 → ((𝑧 ∈ ⦋𝑧 / 𝑥⦌𝐴 ∧ 𝐵 = ⦋𝑧 / 𝑥⦌𝐵) ↔ 𝑥 ∈ 𝐴)) |
9 | 1, 8 | spcev 2807 |
. . 3
⊢ (𝑥 ∈ 𝐴 → ∃𝑧(𝑧 ∈ ⦋𝑧 / 𝑥⦌𝐴 ∧ 𝐵 = ⦋𝑧 / 𝑥⦌𝐵)) |
10 | | df-rex 2441 |
. . . . . 6
⊢
(∃𝑥 ∈
𝐴 𝑦 = 𝐵 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)) |
11 | | nfv 1508 |
. . . . . . 7
⊢
Ⅎ𝑧(𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵) |
12 | | nfcsb1v 3064 |
. . . . . . . . 9
⊢
Ⅎ𝑥⦋𝑧 / 𝑥⦌𝐴 |
13 | 12 | nfcri 2293 |
. . . . . . . 8
⊢
Ⅎ𝑥 𝑧 ∈ ⦋𝑧 / 𝑥⦌𝐴 |
14 | | nfcsb1v 3064 |
. . . . . . . . 9
⊢
Ⅎ𝑥⦋𝑧 / 𝑥⦌𝐵 |
15 | 14 | nfeq2 2311 |
. . . . . . . 8
⊢
Ⅎ𝑥 𝑦 = ⦋𝑧 / 𝑥⦌𝐵 |
16 | 13, 15 | nfan 1545 |
. . . . . . 7
⊢
Ⅎ𝑥(𝑧 ∈ ⦋𝑧 / 𝑥⦌𝐴 ∧ 𝑦 = ⦋𝑧 / 𝑥⦌𝐵) |
17 | 5 | eqeq2d 2169 |
. . . . . . . 8
⊢ (𝑥 = 𝑧 → (𝑦 = 𝐵 ↔ 𝑦 = ⦋𝑧 / 𝑥⦌𝐵)) |
18 | 4, 17 | anbi12d 465 |
. . . . . . 7
⊢ (𝑥 = 𝑧 → ((𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵) ↔ (𝑧 ∈ ⦋𝑧 / 𝑥⦌𝐴 ∧ 𝑦 = ⦋𝑧 / 𝑥⦌𝐵))) |
19 | 11, 16, 18 | cbvex 1736 |
. . . . . 6
⊢
(∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵) ↔ ∃𝑧(𝑧 ∈ ⦋𝑧 / 𝑥⦌𝐴 ∧ 𝑦 = ⦋𝑧 / 𝑥⦌𝐵)) |
20 | 10, 19 | bitri 183 |
. . . . 5
⊢
(∃𝑥 ∈
𝐴 𝑦 = 𝐵 ↔ ∃𝑧(𝑧 ∈ ⦋𝑧 / 𝑥⦌𝐴 ∧ 𝑦 = ⦋𝑧 / 𝑥⦌𝐵)) |
21 | | eqeq1 2164 |
. . . . . . 7
⊢ (𝑦 = 𝐵 → (𝑦 = ⦋𝑧 / 𝑥⦌𝐵 ↔ 𝐵 = ⦋𝑧 / 𝑥⦌𝐵)) |
22 | 21 | anbi2d 460 |
. . . . . 6
⊢ (𝑦 = 𝐵 → ((𝑧 ∈ ⦋𝑧 / 𝑥⦌𝐴 ∧ 𝑦 = ⦋𝑧 / 𝑥⦌𝐵) ↔ (𝑧 ∈ ⦋𝑧 / 𝑥⦌𝐴 ∧ 𝐵 = ⦋𝑧 / 𝑥⦌𝐵))) |
23 | 22 | exbidv 1805 |
. . . . 5
⊢ (𝑦 = 𝐵 → (∃𝑧(𝑧 ∈ ⦋𝑧 / 𝑥⦌𝐴 ∧ 𝑦 = ⦋𝑧 / 𝑥⦌𝐵) ↔ ∃𝑧(𝑧 ∈ ⦋𝑧 / 𝑥⦌𝐴 ∧ 𝐵 = ⦋𝑧 / 𝑥⦌𝐵))) |
24 | 20, 23 | syl5bb 191 |
. . . 4
⊢ (𝑦 = 𝐵 → (∃𝑥 ∈ 𝐴 𝑦 = 𝐵 ↔ ∃𝑧(𝑧 ∈ ⦋𝑧 / 𝑥⦌𝐴 ∧ 𝐵 = ⦋𝑧 / 𝑥⦌𝐵))) |
25 | | rnmpt.1 |
. . . . 5
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) |
26 | 25 | rnmpt 4836 |
. . . 4
⊢ ran 𝐹 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} |
27 | 24, 26 | elab2g 2859 |
. . 3
⊢ (𝐵 ∈ 𝑉 → (𝐵 ∈ ran 𝐹 ↔ ∃𝑧(𝑧 ∈ ⦋𝑧 / 𝑥⦌𝐴 ∧ 𝐵 = ⦋𝑧 / 𝑥⦌𝐵))) |
28 | 9, 27 | syl5ibr 155 |
. 2
⊢ (𝐵 ∈ 𝑉 → (𝑥 ∈ 𝐴 → 𝐵 ∈ ran 𝐹)) |
29 | 28 | impcom 124 |
1
⊢ ((𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝑉) → 𝐵 ∈ ran 𝐹) |