Step | Hyp | Ref
| Expression |
1 | | fnsnr 7001 |
. . . . . . 7
⊢ (𝐹 Fn {𝐴} → (𝑥 ∈ 𝐹 → 𝑥 = 〈𝐴, (𝐹‘𝐴)〉)) |
2 | 1 | adantl 485 |
. . . . . 6
⊢ ((𝐴 ∈ V ∧ 𝐹 Fn {𝐴}) → (𝑥 ∈ 𝐹 → 𝑥 = 〈𝐴, (𝐹‘𝐴)〉)) |
3 | | fnfun 6499 |
. . . . . . . 8
⊢ (𝐹 Fn {𝐴} → Fun 𝐹) |
4 | | snidg 4591 |
. . . . . . . . . 10
⊢ (𝐴 ∈ V → 𝐴 ∈ {𝐴}) |
5 | 4 | adantr 484 |
. . . . . . . . 9
⊢ ((𝐴 ∈ V ∧ 𝐹 Fn {𝐴}) → 𝐴 ∈ {𝐴}) |
6 | | fndm 6502 |
. . . . . . . . . 10
⊢ (𝐹 Fn {𝐴} → dom 𝐹 = {𝐴}) |
7 | 6 | adantl 485 |
. . . . . . . . 9
⊢ ((𝐴 ∈ V ∧ 𝐹 Fn {𝐴}) → dom 𝐹 = {𝐴}) |
8 | 5, 7 | eleqtrrd 2843 |
. . . . . . . 8
⊢ ((𝐴 ∈ V ∧ 𝐹 Fn {𝐴}) → 𝐴 ∈ dom 𝐹) |
9 | | funfvop 6891 |
. . . . . . . 8
⊢ ((Fun
𝐹 ∧ 𝐴 ∈ dom 𝐹) → 〈𝐴, (𝐹‘𝐴)〉 ∈ 𝐹) |
10 | 3, 8, 9 | syl2an2 686 |
. . . . . . 7
⊢ ((𝐴 ∈ V ∧ 𝐹 Fn {𝐴}) → 〈𝐴, (𝐹‘𝐴)〉 ∈ 𝐹) |
11 | | eleq1 2827 |
. . . . . . 7
⊢ (𝑥 = 〈𝐴, (𝐹‘𝐴)〉 → (𝑥 ∈ 𝐹 ↔ 〈𝐴, (𝐹‘𝐴)〉 ∈ 𝐹)) |
12 | 10, 11 | syl5ibrcom 250 |
. . . . . 6
⊢ ((𝐴 ∈ V ∧ 𝐹 Fn {𝐴}) → (𝑥 = 〈𝐴, (𝐹‘𝐴)〉 → 𝑥 ∈ 𝐹)) |
13 | 2, 12 | impbid 215 |
. . . . 5
⊢ ((𝐴 ∈ V ∧ 𝐹 Fn {𝐴}) → (𝑥 ∈ 𝐹 ↔ 𝑥 = 〈𝐴, (𝐹‘𝐴)〉)) |
14 | | velsn 4573 |
. . . . 5
⊢ (𝑥 ∈ {〈𝐴, (𝐹‘𝐴)〉} ↔ 𝑥 = 〈𝐴, (𝐹‘𝐴)〉) |
15 | 13, 14 | bitr4di 292 |
. . . 4
⊢ ((𝐴 ∈ V ∧ 𝐹 Fn {𝐴}) → (𝑥 ∈ 𝐹 ↔ 𝑥 ∈ {〈𝐴, (𝐹‘𝐴)〉})) |
16 | 15 | eqrdv 2737 |
. . 3
⊢ ((𝐴 ∈ V ∧ 𝐹 Fn {𝐴}) → 𝐹 = {〈𝐴, (𝐹‘𝐴)〉}) |
17 | 16 | ex 416 |
. 2
⊢ (𝐴 ∈ V → (𝐹 Fn {𝐴} → 𝐹 = {〈𝐴, (𝐹‘𝐴)〉})) |
18 | | fvex 6751 |
. . . 4
⊢ (𝐹‘𝐴) ∈ V |
19 | | fnsng 6452 |
. . . 4
⊢ ((𝐴 ∈ V ∧ (𝐹‘𝐴) ∈ V) → {〈𝐴, (𝐹‘𝐴)〉} Fn {𝐴}) |
20 | 18, 19 | mpan2 691 |
. . 3
⊢ (𝐴 ∈ V → {〈𝐴, (𝐹‘𝐴)〉} Fn {𝐴}) |
21 | | fneq1 6490 |
. . 3
⊢ (𝐹 = {〈𝐴, (𝐹‘𝐴)〉} → (𝐹 Fn {𝐴} ↔ {〈𝐴, (𝐹‘𝐴)〉} Fn {𝐴})) |
22 | 20, 21 | syl5ibrcom 250 |
. 2
⊢ (𝐴 ∈ V → (𝐹 = {〈𝐴, (𝐹‘𝐴)〉} → 𝐹 Fn {𝐴})) |
23 | 17, 22 | impbid 215 |
1
⊢ (𝐴 ∈ V → (𝐹 Fn {𝐴} ↔ 𝐹 = {〈𝐴, (𝐹‘𝐴)〉})) |