| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | fnprb.a | . . . . . 6
⊢ 𝐴 ∈ V | 
| 2 | 1 | fnsnb 7186 | . . . . 5
⊢ (𝐹 Fn {𝐴} ↔ 𝐹 = {〈𝐴, (𝐹‘𝐴)〉}) | 
| 3 |  | dfsn2 4638 | . . . . . 6
⊢ {𝐴} = {𝐴, 𝐴} | 
| 4 | 3 | fneq2i 6665 | . . . . 5
⊢ (𝐹 Fn {𝐴} ↔ 𝐹 Fn {𝐴, 𝐴}) | 
| 5 |  | dfsn2 4638 | . . . . . 6
⊢
{〈𝐴, (𝐹‘𝐴)〉} = {〈𝐴, (𝐹‘𝐴)〉, 〈𝐴, (𝐹‘𝐴)〉} | 
| 6 | 5 | eqeq2i 2749 | . . . . 5
⊢ (𝐹 = {〈𝐴, (𝐹‘𝐴)〉} ↔ 𝐹 = {〈𝐴, (𝐹‘𝐴)〉, 〈𝐴, (𝐹‘𝐴)〉}) | 
| 7 | 2, 4, 6 | 3bitr3i 301 | . . . 4
⊢ (𝐹 Fn {𝐴, 𝐴} ↔ 𝐹 = {〈𝐴, (𝐹‘𝐴)〉, 〈𝐴, (𝐹‘𝐴)〉}) | 
| 8 | 7 | a1i 11 | . . 3
⊢ (𝐴 = 𝐵 → (𝐹 Fn {𝐴, 𝐴} ↔ 𝐹 = {〈𝐴, (𝐹‘𝐴)〉, 〈𝐴, (𝐹‘𝐴)〉})) | 
| 9 |  | preq2 4733 | . . . 4
⊢ (𝐴 = 𝐵 → {𝐴, 𝐴} = {𝐴, 𝐵}) | 
| 10 | 9 | fneq2d 6661 | . . 3
⊢ (𝐴 = 𝐵 → (𝐹 Fn {𝐴, 𝐴} ↔ 𝐹 Fn {𝐴, 𝐵})) | 
| 11 |  | id 22 | . . . . . 6
⊢ (𝐴 = 𝐵 → 𝐴 = 𝐵) | 
| 12 |  | fveq2 6905 | . . . . . 6
⊢ (𝐴 = 𝐵 → (𝐹‘𝐴) = (𝐹‘𝐵)) | 
| 13 | 11, 12 | opeq12d 4880 | . . . . 5
⊢ (𝐴 = 𝐵 → 〈𝐴, (𝐹‘𝐴)〉 = 〈𝐵, (𝐹‘𝐵)〉) | 
| 14 | 13 | preq2d 4739 | . . . 4
⊢ (𝐴 = 𝐵 → {〈𝐴, (𝐹‘𝐴)〉, 〈𝐴, (𝐹‘𝐴)〉} = {〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}) | 
| 15 | 14 | eqeq2d 2747 | . . 3
⊢ (𝐴 = 𝐵 → (𝐹 = {〈𝐴, (𝐹‘𝐴)〉, 〈𝐴, (𝐹‘𝐴)〉} ↔ 𝐹 = {〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉})) | 
| 16 | 8, 10, 15 | 3bitr3d 309 | . 2
⊢ (𝐴 = 𝐵 → (𝐹 Fn {𝐴, 𝐵} ↔ 𝐹 = {〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉})) | 
| 17 |  | fndm 6670 | . . . . . 6
⊢ (𝐹 Fn {𝐴, 𝐵} → dom 𝐹 = {𝐴, 𝐵}) | 
| 18 |  | fvex 6918 | . . . . . . 7
⊢ (𝐹‘𝐴) ∈ V | 
| 19 |  | fvex 6918 | . . . . . . 7
⊢ (𝐹‘𝐵) ∈ V | 
| 20 | 18, 19 | dmprop 6236 | . . . . . 6
⊢ dom
{〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉} = {𝐴, 𝐵} | 
| 21 | 17, 20 | eqtr4di 2794 | . . . . 5
⊢ (𝐹 Fn {𝐴, 𝐵} → dom 𝐹 = dom {〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}) | 
| 22 | 21 | adantl 481 | . . . 4
⊢ ((𝐴 ≠ 𝐵 ∧ 𝐹 Fn {𝐴, 𝐵}) → dom 𝐹 = dom {〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}) | 
| 23 | 17 | adantl 481 | . . . . . . 7
⊢ ((𝐴 ≠ 𝐵 ∧ 𝐹 Fn {𝐴, 𝐵}) → dom 𝐹 = {𝐴, 𝐵}) | 
| 24 | 23 | eleq2d 2826 | . . . . . 6
⊢ ((𝐴 ≠ 𝐵 ∧ 𝐹 Fn {𝐴, 𝐵}) → (𝑥 ∈ dom 𝐹 ↔ 𝑥 ∈ {𝐴, 𝐵})) | 
| 25 |  | vex 3483 | . . . . . . . 8
⊢ 𝑥 ∈ V | 
| 26 | 25 | elpr 4649 | . . . . . . 7
⊢ (𝑥 ∈ {𝐴, 𝐵} ↔ (𝑥 = 𝐴 ∨ 𝑥 = 𝐵)) | 
| 27 | 1, 18 | fvpr1 7213 | . . . . . . . . . . 11
⊢ (𝐴 ≠ 𝐵 → ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}‘𝐴) = (𝐹‘𝐴)) | 
| 28 | 27 | adantr 480 | . . . . . . . . . 10
⊢ ((𝐴 ≠ 𝐵 ∧ 𝐹 Fn {𝐴, 𝐵}) → ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}‘𝐴) = (𝐹‘𝐴)) | 
| 29 | 28 | eqcomd 2742 | . . . . . . . . 9
⊢ ((𝐴 ≠ 𝐵 ∧ 𝐹 Fn {𝐴, 𝐵}) → (𝐹‘𝐴) = ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}‘𝐴)) | 
| 30 |  | fveq2 6905 | . . . . . . . . . 10
⊢ (𝑥 = 𝐴 → (𝐹‘𝑥) = (𝐹‘𝐴)) | 
| 31 |  | fveq2 6905 | . . . . . . . . . 10
⊢ (𝑥 = 𝐴 → ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}‘𝑥) = ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}‘𝐴)) | 
| 32 | 30, 31 | eqeq12d 2752 | . . . . . . . . 9
⊢ (𝑥 = 𝐴 → ((𝐹‘𝑥) = ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}‘𝑥) ↔ (𝐹‘𝐴) = ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}‘𝐴))) | 
| 33 | 29, 32 | syl5ibrcom 247 | . . . . . . . 8
⊢ ((𝐴 ≠ 𝐵 ∧ 𝐹 Fn {𝐴, 𝐵}) → (𝑥 = 𝐴 → (𝐹‘𝑥) = ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}‘𝑥))) | 
| 34 |  | fnprb.b | . . . . . . . . . . . 12
⊢ 𝐵 ∈ V | 
| 35 | 34, 19 | fvpr2 7214 | . . . . . . . . . . 11
⊢ (𝐴 ≠ 𝐵 → ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}‘𝐵) = (𝐹‘𝐵)) | 
| 36 | 35 | adantr 480 | . . . . . . . . . 10
⊢ ((𝐴 ≠ 𝐵 ∧ 𝐹 Fn {𝐴, 𝐵}) → ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}‘𝐵) = (𝐹‘𝐵)) | 
| 37 | 36 | eqcomd 2742 | . . . . . . . . 9
⊢ ((𝐴 ≠ 𝐵 ∧ 𝐹 Fn {𝐴, 𝐵}) → (𝐹‘𝐵) = ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}‘𝐵)) | 
| 38 |  | fveq2 6905 | . . . . . . . . . 10
⊢ (𝑥 = 𝐵 → (𝐹‘𝑥) = (𝐹‘𝐵)) | 
| 39 |  | fveq2 6905 | . . . . . . . . . 10
⊢ (𝑥 = 𝐵 → ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}‘𝑥) = ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}‘𝐵)) | 
| 40 | 38, 39 | eqeq12d 2752 | . . . . . . . . 9
⊢ (𝑥 = 𝐵 → ((𝐹‘𝑥) = ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}‘𝑥) ↔ (𝐹‘𝐵) = ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}‘𝐵))) | 
| 41 | 37, 40 | syl5ibrcom 247 | . . . . . . . 8
⊢ ((𝐴 ≠ 𝐵 ∧ 𝐹 Fn {𝐴, 𝐵}) → (𝑥 = 𝐵 → (𝐹‘𝑥) = ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}‘𝑥))) | 
| 42 | 33, 41 | jaod 859 | . . . . . . 7
⊢ ((𝐴 ≠ 𝐵 ∧ 𝐹 Fn {𝐴, 𝐵}) → ((𝑥 = 𝐴 ∨ 𝑥 = 𝐵) → (𝐹‘𝑥) = ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}‘𝑥))) | 
| 43 | 26, 42 | biimtrid 242 | . . . . . 6
⊢ ((𝐴 ≠ 𝐵 ∧ 𝐹 Fn {𝐴, 𝐵}) → (𝑥 ∈ {𝐴, 𝐵} → (𝐹‘𝑥) = ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}‘𝑥))) | 
| 44 | 24, 43 | sylbid 240 | . . . . 5
⊢ ((𝐴 ≠ 𝐵 ∧ 𝐹 Fn {𝐴, 𝐵}) → (𝑥 ∈ dom 𝐹 → (𝐹‘𝑥) = ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}‘𝑥))) | 
| 45 | 44 | ralrimiv 3144 | . . . 4
⊢ ((𝐴 ≠ 𝐵 ∧ 𝐹 Fn {𝐴, 𝐵}) → ∀𝑥 ∈ dom 𝐹(𝐹‘𝑥) = ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}‘𝑥)) | 
| 46 |  | fnfun 6667 | . . . . 5
⊢ (𝐹 Fn {𝐴, 𝐵} → Fun 𝐹) | 
| 47 | 1, 34, 18, 19 | funpr 6621 | . . . . 5
⊢ (𝐴 ≠ 𝐵 → Fun {〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}) | 
| 48 |  | eqfunfv 7055 | . . . . 5
⊢ ((Fun
𝐹 ∧ Fun {〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}) → (𝐹 = {〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉} ↔ (dom 𝐹 = dom {〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉} ∧ ∀𝑥 ∈ dom 𝐹(𝐹‘𝑥) = ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}‘𝑥)))) | 
| 49 | 46, 47, 48 | syl2anr 597 | . . . 4
⊢ ((𝐴 ≠ 𝐵 ∧ 𝐹 Fn {𝐴, 𝐵}) → (𝐹 = {〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉} ↔ (dom 𝐹 = dom {〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉} ∧ ∀𝑥 ∈ dom 𝐹(𝐹‘𝑥) = ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}‘𝑥)))) | 
| 50 | 22, 45, 49 | mpbir2and 713 | . . 3
⊢ ((𝐴 ≠ 𝐵 ∧ 𝐹 Fn {𝐴, 𝐵}) → 𝐹 = {〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}) | 
| 51 |  | df-fn 6563 | . . . . 5
⊢
({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉} Fn {𝐴, 𝐵} ↔ (Fun {〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉} ∧ dom {〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉} = {𝐴, 𝐵})) | 
| 52 | 47, 20, 51 | sylanblrc 590 | . . . 4
⊢ (𝐴 ≠ 𝐵 → {〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉} Fn {𝐴, 𝐵}) | 
| 53 |  | fneq1 6658 | . . . . 5
⊢ (𝐹 = {〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉} → (𝐹 Fn {𝐴, 𝐵} ↔ {〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉} Fn {𝐴, 𝐵})) | 
| 54 | 53 | biimprd 248 | . . . 4
⊢ (𝐹 = {〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉} → ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉} Fn {𝐴, 𝐵} → 𝐹 Fn {𝐴, 𝐵})) | 
| 55 | 52, 54 | mpan9 506 | . . 3
⊢ ((𝐴 ≠ 𝐵 ∧ 𝐹 = {〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}) → 𝐹 Fn {𝐴, 𝐵}) | 
| 56 | 50, 55 | impbida 800 | . 2
⊢ (𝐴 ≠ 𝐵 → (𝐹 Fn {𝐴, 𝐵} ↔ 𝐹 = {〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉})) | 
| 57 | 16, 56 | pm2.61ine 3024 | 1
⊢ (𝐹 Fn {𝐴, 𝐵} ↔ 𝐹 = {〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}) |