| Step | Hyp | Ref
| Expression |
| 1 | | tru 1544 |
. . . . 5
⊢
⊤ |
| 2 | | csbeq1a 3913 |
. . . . . . . 8
⊢ (𝑥 = 𝑧 → 𝐵 = ⦋𝑧 / 𝑥⦌𝐵) |
| 3 | 2 | equcoms 2019 |
. . . . . . 7
⊢ (𝑧 = 𝑥 → 𝐵 = ⦋𝑧 / 𝑥⦌𝐵) |
| 4 | | trud 1550 |
. . . . . . 7
⊢ (𝑧 = 𝑥 → ⊤) |
| 5 | 3, 4 | 2thd 265 |
. . . . . 6
⊢ (𝑧 = 𝑥 → (𝐵 = ⦋𝑧 / 𝑥⦌𝐵 ↔ ⊤)) |
| 6 | 5 | rspcev 3622 |
. . . . 5
⊢ ((𝑥 ∈ 𝐴 ∧ ⊤) → ∃𝑧 ∈ 𝐴 𝐵 = ⦋𝑧 / 𝑥⦌𝐵) |
| 7 | 1, 6 | mpan2 691 |
. . . 4
⊢ (𝑥 ∈ 𝐴 → ∃𝑧 ∈ 𝐴 𝐵 = ⦋𝑧 / 𝑥⦌𝐵) |
| 8 | 7 | adantr 480 |
. . 3
⊢ ((𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝑉) → ∃𝑧 ∈ 𝐴 𝐵 = ⦋𝑧 / 𝑥⦌𝐵) |
| 9 | | eqeq1 2741 |
. . . . . 6
⊢ (𝑦 = 𝐵 → (𝑦 = ⦋𝑧 / 𝑥⦌𝐵 ↔ 𝐵 = ⦋𝑧 / 𝑥⦌𝐵)) |
| 10 | 9 | rexbidv 3179 |
. . . . 5
⊢ (𝑦 = 𝐵 → (∃𝑧 ∈ 𝐴 𝑦 = ⦋𝑧 / 𝑥⦌𝐵 ↔ ∃𝑧 ∈ 𝐴 𝐵 = ⦋𝑧 / 𝑥⦌𝐵)) |
| 11 | 10 | elabg 3676 |
. . . 4
⊢ (𝐵 ∈ 𝑉 → (𝐵 ∈ {𝑦 ∣ ∃𝑧 ∈ 𝐴 𝑦 = ⦋𝑧 / 𝑥⦌𝐵} ↔ ∃𝑧 ∈ 𝐴 𝐵 = ⦋𝑧 / 𝑥⦌𝐵)) |
| 12 | 11 | adantl 481 |
. . 3
⊢ ((𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝑉) → (𝐵 ∈ {𝑦 ∣ ∃𝑧 ∈ 𝐴 𝑦 = ⦋𝑧 / 𝑥⦌𝐵} ↔ ∃𝑧 ∈ 𝐴 𝐵 = ⦋𝑧 / 𝑥⦌𝐵)) |
| 13 | 8, 12 | mpbird 257 |
. 2
⊢ ((𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝑉) → 𝐵 ∈ {𝑦 ∣ ∃𝑧 ∈ 𝐴 𝑦 = ⦋𝑧 / 𝑥⦌𝐵}) |
| 14 | | nfv 1914 |
. . . 4
⊢
Ⅎ𝑧 𝑦 = 𝐵 |
| 15 | | nfcsb1v 3923 |
. . . . 5
⊢
Ⅎ𝑥⦋𝑧 / 𝑥⦌𝐵 |
| 16 | 15 | nfeq2 2923 |
. . . 4
⊢
Ⅎ𝑥 𝑦 = ⦋𝑧 / 𝑥⦌𝐵 |
| 17 | 2 | eqeq2d 2748 |
. . . 4
⊢ (𝑥 = 𝑧 → (𝑦 = 𝐵 ↔ 𝑦 = ⦋𝑧 / 𝑥⦌𝐵)) |
| 18 | 14, 16, 17 | cbvrexw 3307 |
. . 3
⊢
(∃𝑥 ∈
𝐴 𝑦 = 𝐵 ↔ ∃𝑧 ∈ 𝐴 𝑦 = ⦋𝑧 / 𝑥⦌𝐵) |
| 19 | 18 | abbii 2809 |
. 2
⊢ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} = {𝑦 ∣ ∃𝑧 ∈ 𝐴 𝑦 = ⦋𝑧 / 𝑥⦌𝐵} |
| 20 | 13, 19 | eleqtrrdi 2852 |
1
⊢ ((𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝑉) → 𝐵 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵}) |