| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | opelf 6768 | . . . . . . . 8
⊢ ((𝐹:{𝐴}⟶{𝐵} ∧ 〈𝑥, 𝑦〉 ∈ 𝐹) → (𝑥 ∈ {𝐴} ∧ 𝑦 ∈ {𝐵})) | 
| 2 |  | velsn 4641 | . . . . . . . . 9
⊢ (𝑥 ∈ {𝐴} ↔ 𝑥 = 𝐴) | 
| 3 |  | velsn 4641 | . . . . . . . . 9
⊢ (𝑦 ∈ {𝐵} ↔ 𝑦 = 𝐵) | 
| 4 | 2, 3 | anbi12i 628 | . . . . . . . 8
⊢ ((𝑥 ∈ {𝐴} ∧ 𝑦 ∈ {𝐵}) ↔ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) | 
| 5 | 1, 4 | sylib 218 | . . . . . . 7
⊢ ((𝐹:{𝐴}⟶{𝐵} ∧ 〈𝑥, 𝑦〉 ∈ 𝐹) → (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) | 
| 6 | 5 | ex 412 | . . . . . 6
⊢ (𝐹:{𝐴}⟶{𝐵} → (〈𝑥, 𝑦〉 ∈ 𝐹 → (𝑥 = 𝐴 ∧ 𝑦 = 𝐵))) | 
| 7 |  | fsn.1 | . . . . . . . . . 10
⊢ 𝐴 ∈ V | 
| 8 | 7 | snid 4661 | . . . . . . . . 9
⊢ 𝐴 ∈ {𝐴} | 
| 9 |  | feu 6783 | . . . . . . . . 9
⊢ ((𝐹:{𝐴}⟶{𝐵} ∧ 𝐴 ∈ {𝐴}) → ∃!𝑦 ∈ {𝐵}〈𝐴, 𝑦〉 ∈ 𝐹) | 
| 10 | 8, 9 | mpan2 691 | . . . . . . . 8
⊢ (𝐹:{𝐴}⟶{𝐵} → ∃!𝑦 ∈ {𝐵}〈𝐴, 𝑦〉 ∈ 𝐹) | 
| 11 | 3 | anbi1i 624 | . . . . . . . . . . 11
⊢ ((𝑦 ∈ {𝐵} ∧ 〈𝐴, 𝑦〉 ∈ 𝐹) ↔ (𝑦 = 𝐵 ∧ 〈𝐴, 𝑦〉 ∈ 𝐹)) | 
| 12 |  | opeq2 4873 | . . . . . . . . . . . . . 14
⊢ (𝑦 = 𝐵 → 〈𝐴, 𝑦〉 = 〈𝐴, 𝐵〉) | 
| 13 | 12 | eleq1d 2825 | . . . . . . . . . . . . 13
⊢ (𝑦 = 𝐵 → (〈𝐴, 𝑦〉 ∈ 𝐹 ↔ 〈𝐴, 𝐵〉 ∈ 𝐹)) | 
| 14 | 13 | pm5.32i 574 | . . . . . . . . . . . 12
⊢ ((𝑦 = 𝐵 ∧ 〈𝐴, 𝑦〉 ∈ 𝐹) ↔ (𝑦 = 𝐵 ∧ 〈𝐴, 𝐵〉 ∈ 𝐹)) | 
| 15 | 14 | biancomi 462 | . . . . . . . . . . 11
⊢ ((𝑦 = 𝐵 ∧ 〈𝐴, 𝑦〉 ∈ 𝐹) ↔ (〈𝐴, 𝐵〉 ∈ 𝐹 ∧ 𝑦 = 𝐵)) | 
| 16 | 11, 15 | bitr2i 276 | . . . . . . . . . 10
⊢
((〈𝐴, 𝐵〉 ∈ 𝐹 ∧ 𝑦 = 𝐵) ↔ (𝑦 ∈ {𝐵} ∧ 〈𝐴, 𝑦〉 ∈ 𝐹)) | 
| 17 | 16 | eubii 2584 | . . . . . . . . 9
⊢
(∃!𝑦(〈𝐴, 𝐵〉 ∈ 𝐹 ∧ 𝑦 = 𝐵) ↔ ∃!𝑦(𝑦 ∈ {𝐵} ∧ 〈𝐴, 𝑦〉 ∈ 𝐹)) | 
| 18 |  | fsn.2 | . . . . . . . . . . . 12
⊢ 𝐵 ∈ V | 
| 19 | 18 | eueqi 3714 | . . . . . . . . . . 11
⊢
∃!𝑦 𝑦 = 𝐵 | 
| 20 | 19 | biantru 529 | . . . . . . . . . 10
⊢
(〈𝐴, 𝐵〉 ∈ 𝐹 ↔ (〈𝐴, 𝐵〉 ∈ 𝐹 ∧ ∃!𝑦 𝑦 = 𝐵)) | 
| 21 |  | euanv 2623 | . . . . . . . . . 10
⊢
(∃!𝑦(〈𝐴, 𝐵〉 ∈ 𝐹 ∧ 𝑦 = 𝐵) ↔ (〈𝐴, 𝐵〉 ∈ 𝐹 ∧ ∃!𝑦 𝑦 = 𝐵)) | 
| 22 | 20, 21 | bitr4i 278 | . . . . . . . . 9
⊢
(〈𝐴, 𝐵〉 ∈ 𝐹 ↔ ∃!𝑦(〈𝐴, 𝐵〉 ∈ 𝐹 ∧ 𝑦 = 𝐵)) | 
| 23 |  | df-reu 3380 | . . . . . . . . 9
⊢
(∃!𝑦 ∈
{𝐵}〈𝐴, 𝑦〉 ∈ 𝐹 ↔ ∃!𝑦(𝑦 ∈ {𝐵} ∧ 〈𝐴, 𝑦〉 ∈ 𝐹)) | 
| 24 | 17, 22, 23 | 3bitr4i 303 | . . . . . . . 8
⊢
(〈𝐴, 𝐵〉 ∈ 𝐹 ↔ ∃!𝑦 ∈ {𝐵}〈𝐴, 𝑦〉 ∈ 𝐹) | 
| 25 | 10, 24 | sylibr 234 | . . . . . . 7
⊢ (𝐹:{𝐴}⟶{𝐵} → 〈𝐴, 𝐵〉 ∈ 𝐹) | 
| 26 |  | opeq12 4874 | . . . . . . . 8
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → 〈𝑥, 𝑦〉 = 〈𝐴, 𝐵〉) | 
| 27 | 26 | eleq1d 2825 | . . . . . . 7
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (〈𝑥, 𝑦〉 ∈ 𝐹 ↔ 〈𝐴, 𝐵〉 ∈ 𝐹)) | 
| 28 | 25, 27 | syl5ibrcom 247 | . . . . . 6
⊢ (𝐹:{𝐴}⟶{𝐵} → ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → 〈𝑥, 𝑦〉 ∈ 𝐹)) | 
| 29 | 6, 28 | impbid 212 | . . . . 5
⊢ (𝐹:{𝐴}⟶{𝐵} → (〈𝑥, 𝑦〉 ∈ 𝐹 ↔ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵))) | 
| 30 |  | opex 5468 | . . . . . . 7
⊢
〈𝑥, 𝑦〉 ∈ V | 
| 31 | 30 | elsn 4640 | . . . . . 6
⊢
(〈𝑥, 𝑦〉 ∈ {〈𝐴, 𝐵〉} ↔ 〈𝑥, 𝑦〉 = 〈𝐴, 𝐵〉) | 
| 32 | 7, 18 | opth2 5484 | . . . . . 6
⊢
(〈𝑥, 𝑦〉 = 〈𝐴, 𝐵〉 ↔ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) | 
| 33 | 31, 32 | bitr2i 276 | . . . . 5
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) ↔ 〈𝑥, 𝑦〉 ∈ {〈𝐴, 𝐵〉}) | 
| 34 | 29, 33 | bitrdi 287 | . . . 4
⊢ (𝐹:{𝐴}⟶{𝐵} → (〈𝑥, 𝑦〉 ∈ 𝐹 ↔ 〈𝑥, 𝑦〉 ∈ {〈𝐴, 𝐵〉})) | 
| 35 | 34 | alrimivv 1927 | . . 3
⊢ (𝐹:{𝐴}⟶{𝐵} → ∀𝑥∀𝑦(〈𝑥, 𝑦〉 ∈ 𝐹 ↔ 〈𝑥, 𝑦〉 ∈ {〈𝐴, 𝐵〉})) | 
| 36 |  | frel 6740 | . . . 4
⊢ (𝐹:{𝐴}⟶{𝐵} → Rel 𝐹) | 
| 37 | 7, 18 | relsnop 5814 | . . . 4
⊢ Rel
{〈𝐴, 𝐵〉} | 
| 38 |  | eqrel 5793 | . . . 4
⊢ ((Rel
𝐹 ∧ Rel {〈𝐴, 𝐵〉}) → (𝐹 = {〈𝐴, 𝐵〉} ↔ ∀𝑥∀𝑦(〈𝑥, 𝑦〉 ∈ 𝐹 ↔ 〈𝑥, 𝑦〉 ∈ {〈𝐴, 𝐵〉}))) | 
| 39 | 36, 37, 38 | sylancl 586 | . . 3
⊢ (𝐹:{𝐴}⟶{𝐵} → (𝐹 = {〈𝐴, 𝐵〉} ↔ ∀𝑥∀𝑦(〈𝑥, 𝑦〉 ∈ 𝐹 ↔ 〈𝑥, 𝑦〉 ∈ {〈𝐴, 𝐵〉}))) | 
| 40 | 35, 39 | mpbird 257 | . 2
⊢ (𝐹:{𝐴}⟶{𝐵} → 𝐹 = {〈𝐴, 𝐵〉}) | 
| 41 | 7, 18 | f1osn 6887 | . . . 4
⊢
{〈𝐴, 𝐵〉}:{𝐴}–1-1-onto→{𝐵} | 
| 42 |  | f1oeq1 6835 | . . . 4
⊢ (𝐹 = {〈𝐴, 𝐵〉} → (𝐹:{𝐴}–1-1-onto→{𝐵} ↔ {〈𝐴, 𝐵〉}:{𝐴}–1-1-onto→{𝐵})) | 
| 43 | 41, 42 | mpbiri 258 | . . 3
⊢ (𝐹 = {〈𝐴, 𝐵〉} → 𝐹:{𝐴}–1-1-onto→{𝐵}) | 
| 44 |  | f1of 6847 | . . 3
⊢ (𝐹:{𝐴}–1-1-onto→{𝐵} → 𝐹:{𝐴}⟶{𝐵}) | 
| 45 | 43, 44 | syl 17 | . 2
⊢ (𝐹 = {〈𝐴, 𝐵〉} → 𝐹:{𝐴}⟶{𝐵}) | 
| 46 | 40, 45 | impbii 209 | 1
⊢ (𝐹:{𝐴}⟶{𝐵} ↔ 𝐹 = {〈𝐴, 𝐵〉}) |