Step | Hyp | Ref
| Expression |
1 | | fnsnr 7112 |
. . . . . . 7
⊢ (𝐹 Fn {𝐴} → (𝑥 ∈ 𝐹 → 𝑥 = ⟨𝐴, (𝐹‘𝐴)⟩)) |
2 | 1 | adantl 483 |
. . . . . 6
⊢ ((𝐴 ∈ V ∧ 𝐹 Fn {𝐴}) → (𝑥 ∈ 𝐹 → 𝑥 = ⟨𝐴, (𝐹‘𝐴)⟩)) |
3 | | fnfun 6603 |
. . . . . . . 8
⊢ (𝐹 Fn {𝐴} → Fun 𝐹) |
4 | | snidg 4621 |
. . . . . . . . . 10
⊢ (𝐴 ∈ V → 𝐴 ∈ {𝐴}) |
5 | 4 | adantr 482 |
. . . . . . . . 9
⊢ ((𝐴 ∈ V ∧ 𝐹 Fn {𝐴}) → 𝐴 ∈ {𝐴}) |
6 | | fndm 6606 |
. . . . . . . . . 10
⊢ (𝐹 Fn {𝐴} → dom 𝐹 = {𝐴}) |
7 | 6 | adantl 483 |
. . . . . . . . 9
⊢ ((𝐴 ∈ V ∧ 𝐹 Fn {𝐴}) → dom 𝐹 = {𝐴}) |
8 | 5, 7 | eleqtrrd 2841 |
. . . . . . . 8
⊢ ((𝐴 ∈ V ∧ 𝐹 Fn {𝐴}) → 𝐴 ∈ dom 𝐹) |
9 | | funfvop 7001 |
. . . . . . . 8
⊢ ((Fun
𝐹 ∧ 𝐴 ∈ dom 𝐹) → ⟨𝐴, (𝐹‘𝐴)⟩ ∈ 𝐹) |
10 | 3, 8, 9 | syl2an2 685 |
. . . . . . 7
⊢ ((𝐴 ∈ V ∧ 𝐹 Fn {𝐴}) → ⟨𝐴, (𝐹‘𝐴)⟩ ∈ 𝐹) |
11 | | eleq1 2826 |
. . . . . . 7
⊢ (𝑥 = ⟨𝐴, (𝐹‘𝐴)⟩ → (𝑥 ∈ 𝐹 ↔ ⟨𝐴, (𝐹‘𝐴)⟩ ∈ 𝐹)) |
12 | 10, 11 | syl5ibrcom 247 |
. . . . . 6
⊢ ((𝐴 ∈ V ∧ 𝐹 Fn {𝐴}) → (𝑥 = ⟨𝐴, (𝐹‘𝐴)⟩ → 𝑥 ∈ 𝐹)) |
13 | 2, 12 | impbid 211 |
. . . . 5
⊢ ((𝐴 ∈ V ∧ 𝐹 Fn {𝐴}) → (𝑥 ∈ 𝐹 ↔ 𝑥 = ⟨𝐴, (𝐹‘𝐴)⟩)) |
14 | | velsn 4603 |
. . . . 5
⊢ (𝑥 ∈ {⟨𝐴, (𝐹‘𝐴)⟩} ↔ 𝑥 = ⟨𝐴, (𝐹‘𝐴)⟩) |
15 | 13, 14 | bitr4di 289 |
. . . 4
⊢ ((𝐴 ∈ V ∧ 𝐹 Fn {𝐴}) → (𝑥 ∈ 𝐹 ↔ 𝑥 ∈ {⟨𝐴, (𝐹‘𝐴)⟩})) |
16 | 15 | eqrdv 2735 |
. . 3
⊢ ((𝐴 ∈ V ∧ 𝐹 Fn {𝐴}) → 𝐹 = {⟨𝐴, (𝐹‘𝐴)⟩}) |
17 | 16 | ex 414 |
. 2
⊢ (𝐴 ∈ V → (𝐹 Fn {𝐴} → 𝐹 = {⟨𝐴, (𝐹‘𝐴)⟩})) |
18 | | fvex 6856 |
. . . 4
⊢ (𝐹‘𝐴) ∈ V |
19 | | fnsng 6554 |
. . . 4
⊢ ((𝐴 ∈ V ∧ (𝐹‘𝐴) ∈ V) → {⟨𝐴, (𝐹‘𝐴)⟩} Fn {𝐴}) |
20 | 18, 19 | mpan2 690 |
. . 3
⊢ (𝐴 ∈ V → {⟨𝐴, (𝐹‘𝐴)⟩} Fn {𝐴}) |
21 | | fneq1 6594 |
. . 3
⊢ (𝐹 = {⟨𝐴, (𝐹‘𝐴)⟩} → (𝐹 Fn {𝐴} ↔ {⟨𝐴, (𝐹‘𝐴)⟩} Fn {𝐴})) |
22 | 20, 21 | syl5ibrcom 247 |
. 2
⊢ (𝐴 ∈ V → (𝐹 = {⟨𝐴, (𝐹‘𝐴)⟩} → 𝐹 Fn {𝐴})) |
23 | 17, 22 | impbid 211 |
1
⊢ (𝐴 ∈ V → (𝐹 Fn {𝐴} ↔ 𝐹 = {⟨𝐴, (𝐹‘𝐴)⟩})) |