Step | Hyp | Ref
| Expression |
1 | | fnrnfv 6723 |
. . 3
⊢ (𝐹 Fn 𝐴 → ran 𝐹 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥)}) |
2 | 1 | eleq2d 2818 |
. 2
⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ ran 𝐹 ↔ 𝐵 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥)})) |
3 | | fvex 6681 |
. . . . 5
⊢ (𝐹‘𝑥) ∈ V |
4 | | eleq1 2820 |
. . . . 5
⊢ ((𝐹‘𝑥) = 𝐵 → ((𝐹‘𝑥) ∈ V ↔ 𝐵 ∈ V)) |
5 | 3, 4 | mpbii 236 |
. . . 4
⊢ ((𝐹‘𝑥) = 𝐵 → 𝐵 ∈ V) |
6 | 5 | rexlimivw 3191 |
. . 3
⊢
(∃𝑥 ∈
𝐴 (𝐹‘𝑥) = 𝐵 → 𝐵 ∈ V) |
7 | | eqeq1 2742 |
. . . . 5
⊢ (𝑦 = 𝐵 → (𝑦 = (𝐹‘𝑥) ↔ 𝐵 = (𝐹‘𝑥))) |
8 | | eqcom 2745 |
. . . . 5
⊢ (𝐵 = (𝐹‘𝑥) ↔ (𝐹‘𝑥) = 𝐵) |
9 | 7, 8 | bitrdi 290 |
. . . 4
⊢ (𝑦 = 𝐵 → (𝑦 = (𝐹‘𝑥) ↔ (𝐹‘𝑥) = 𝐵)) |
10 | 9 | rexbidv 3206 |
. . 3
⊢ (𝑦 = 𝐵 → (∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥) ↔ ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝐵)) |
11 | 6, 10 | elab3 3578 |
. 2
⊢ (𝐵 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥)} ↔ ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝐵) |
12 | 2, 11 | bitrdi 290 |
1
⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝐵)) |