Step | Hyp | Ref
| Expression |
1 | | funfvop 5222 |
. . . . . 6
⊢ ((Fun
𝐹 ∧ A ∈ dom 𝐹) → 〈A, (𝐹‘A)〉 ∈ 𝐹) |
2 | | ssel 2933 |
. . . . . 6
⊢ (𝐹 ⊆ 𝐺 → (〈A, (𝐹‘A)〉 ∈ 𝐹 → 〈A, (𝐹‘A)〉 ∈ 𝐺)) |
3 | 1, 2 | syl5 28 |
. . . . 5
⊢ (𝐹 ⊆ 𝐺 → ((Fun 𝐹 ∧ A ∈ dom 𝐹) → 〈A, (𝐹‘A)〉 ∈ 𝐺)) |
4 | 3 | imp 115 |
. . . 4
⊢ ((𝐹 ⊆ 𝐺 ∧ (Fun
𝐹 ∧ A ∈ dom 𝐹)) → 〈A, (𝐹‘A)〉 ∈ 𝐺) |
5 | | simpr 103 |
. . . . . 6
⊢ ((Fun
𝐹 ∧ A ∈ dom 𝐹) → A ∈ dom 𝐹) |
6 | | sneq 3378 |
. . . . . . . . . 10
⊢ (x = A →
{x} = {A}) |
7 | 6 | imaeq2d 4611 |
. . . . . . . . 9
⊢ (x = A →
(𝐺 “ {x}) = (𝐺 “ {A})) |
8 | 7 | eleq2d 2104 |
. . . . . . . 8
⊢ (x = A →
((𝐹‘A) ∈ (𝐺 “ {x}) ↔ (𝐹‘A) ∈ (𝐺 “ {A}))) |
9 | | opeq1 3540 |
. . . . . . . . 9
⊢ (x = A →
〈x, (𝐹‘A)〉 = 〈A, (𝐹‘A)〉) |
10 | 9 | eleq1d 2103 |
. . . . . . . 8
⊢ (x = A →
(〈x, (𝐹‘A)〉 ∈ 𝐺 ↔ 〈A, (𝐹‘A)〉 ∈ 𝐺)) |
11 | 8, 10 | bibi12d 224 |
. . . . . . 7
⊢ (x = A →
(((𝐹‘A) ∈ (𝐺 “ {x}) ↔ 〈x, (𝐹‘A)〉 ∈ 𝐺) ↔ ((𝐹‘A) ∈ (𝐺 “ {A}) ↔ 〈A, (𝐹‘A)〉 ∈ 𝐺))) |
12 | 11 | adantl 262 |
. . . . . 6
⊢ (((Fun
𝐹 ∧ A ∈ dom 𝐹) ∧
x = A)
→ (((𝐹‘A) ∈ (𝐺 “ {x}) ↔ 〈x, (𝐹‘A)〉 ∈ 𝐺) ↔ ((𝐹‘A) ∈ (𝐺 “ {A}) ↔ 〈A, (𝐹‘A)〉 ∈ 𝐺))) |
13 | | vex 2554 |
. . . . . . 7
⊢ x ∈
V |
14 | | funfvex 5135 |
. . . . . . 7
⊢ ((Fun
𝐹 ∧ A ∈ dom 𝐹) → (𝐹‘A) ∈
V) |
15 | | elimasng 4636 |
. . . . . . 7
⊢
((x ∈ V ∧ (𝐹‘A) ∈ V) →
((𝐹‘A) ∈ (𝐺 “ {x}) ↔ 〈x, (𝐹‘A)〉 ∈ 𝐺)) |
16 | 13, 14, 15 | sylancr 393 |
. . . . . 6
⊢ ((Fun
𝐹 ∧ A ∈ dom 𝐹) → ((𝐹‘A) ∈ (𝐺 “ {x}) ↔ 〈x, (𝐹‘A)〉 ∈ 𝐺)) |
17 | 5, 12, 16 | vtocld 2600 |
. . . . 5
⊢ ((Fun
𝐹 ∧ A ∈ dom 𝐹) → ((𝐹‘A) ∈ (𝐺 “ {A}) ↔ 〈A, (𝐹‘A)〉 ∈ 𝐺)) |
18 | 17 | adantl 262 |
. . . 4
⊢ ((𝐹 ⊆ 𝐺 ∧ (Fun
𝐹 ∧ A ∈ dom 𝐹)) → ((𝐹‘A) ∈ (𝐺 “ {A}) ↔ 〈A, (𝐹‘A)〉 ∈ 𝐺)) |
19 | 4, 18 | mpbird 156 |
. . 3
⊢ ((𝐹 ⊆ 𝐺 ∧ (Fun
𝐹 ∧ A ∈ dom 𝐹)) → (𝐹‘A) ∈ (𝐺 “ {A})) |
20 | 19 | exp32 347 |
. 2
⊢ (𝐹 ⊆ 𝐺 → (Fun 𝐹 → (A ∈ dom 𝐹 → (𝐹‘A) ∈ (𝐺 “ {A})))) |
21 | 20 | impcom 116 |
1
⊢ ((Fun
𝐹 ∧ 𝐹 ⊆ 𝐺) → (A ∈ dom 𝐹 → (𝐹‘A) ∈ (𝐺 “ {A}))) |