Theorem fresunsn 33267

Description: Recover the original function from a point-added function. See also funresdfunsn 7195 and fsnunres 7194. (Contributed by Thierry Arnoux, 15-Feb-2026.)

Assertion

Ref	Expression
fresunsn	⊢ ((𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ (𝐹‘𝑋) = 𝑌) → ((𝐹 ↾ (𝐴 ∖ {𝑋})) ∪ {⟨𝑋, 𝑌⟩}) = 𝐹)

Proof of Theorem fresunsn

Step	Hyp	Ref	Expression
1		resdmdfsn 6020	. . . 4 ⊢ (𝐹 ↾ (V ∖ {𝑋})) = (𝐹 ↾ (dom 𝐹 ∖ {𝑋}))
2		fndm 6643	. . . . . . 7 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
3	2	3ad2ant1 1151	. . . . . 6 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ (𝐹‘𝑋) = 𝑌) → dom 𝐹 = 𝐴)
4	3	difeq1d 4062	. . . . 5 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ (𝐹‘𝑋) = 𝑌) → (dom 𝐹 ∖ {𝑋}) = (𝐴 ∖ {𝑋}))
5	4	reseq2d 5969	. . . 4 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ (𝐹‘𝑋) = 𝑌) → (𝐹 ↾ (dom 𝐹 ∖ {𝑋})) = (𝐹 ↾ (𝐴 ∖ {𝑋})))
6	1, 5	eqtr2id 2808	. . 3 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ (𝐹‘𝑋) = 𝑌) → (𝐹 ↾ (𝐴 ∖ {𝑋})) = (𝐹 ↾ (V ∖ {𝑋})))
7		simp3 1156	. . . . . 6 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ (𝐹‘𝑋) = 𝑌) → (𝐹‘𝑋) = 𝑌)
8	7	eqcomd 2766	. . . . 5 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ (𝐹‘𝑋) = 𝑌) → 𝑌 = (𝐹‘𝑋))
9	8	opeq2d 4846	. . . 4 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ (𝐹‘𝑋) = 𝑌) → ⟨𝑋, 𝑌⟩ = ⟨𝑋, (𝐹‘𝑋)⟩)
10	9	sneqd 4592	. . 3 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ (𝐹‘𝑋) = 𝑌) → {⟨𝑋, 𝑌⟩} = {⟨𝑋, (𝐹‘𝑋)⟩})
11	6, 10	uneq12d 4168	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ (𝐹‘𝑋) = 𝑌) → ((𝐹 ↾ (𝐴 ∖ {𝑋})) ∪ {⟨𝑋, 𝑌⟩}) = ((𝐹 ↾ (V ∖ {𝑋})) ∪ {⟨𝑋, (𝐹‘𝑋)⟩}))
12		fnfun 6640	. . . 4 ⊢ (𝐹 Fn 𝐴 → Fun 𝐹)
13	12	3ad2ant1 1151	. . 3 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ (𝐹‘𝑋) = 𝑌) → Fun 𝐹)
14	2	eleq2d 2846	. . . . 5 ⊢ (𝐹 Fn 𝐴 → (𝑋 ∈ dom 𝐹 ↔ 𝑋 ∈ 𝐴))
15	14	biimpar 483	. . . 4 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → 𝑋 ∈ dom 𝐹)
16	15	3adant3 1150	. . 3 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ (𝐹‘𝑋) = 𝑌) → 𝑋 ∈ dom 𝐹)
17		funresdfunsn 7195	. . 3 ⊢ ((Fun 𝐹 ∧ 𝑋 ∈ dom 𝐹) → ((𝐹 ↾ (V ∖ {𝑋})) ∪ {⟨𝑋, (𝐹‘𝑋)⟩}) = 𝐹)
18	13, 16, 17	syl2anc 596	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ (𝐹‘𝑋) = 𝑌) → ((𝐹 ↾ (V ∖ {𝑋})) ∪ {⟨𝑋, (𝐹‘𝑋)⟩}) = 𝐹)
19	11, 18	eqtrd 2795	1 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ (𝐹‘𝑋) = 𝑌) → ((𝐹 ↾ (𝐴 ∖ {𝑋})) ∪ {⟨𝑋, 𝑌⟩}) = 𝐹)

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103   = wceq 1569   ∈ wcel 2144  Vcvv 3450   ∖ cdif 4045   ∪ cun 4149  {csn 4584  ⟨cop 4834  dom cdm 5650   ↾ cres 5652  Fun wfun 6533   Fn wfn 6534  ‘cfv 6539

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pr 5390

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-ral 3077  df-rex 3087  df-reu 3366  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-opab 5167  df-id 5545  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663  df-iota 6494  df-fun 6541  df-fn 6542  df-f 6543  df-f1 6544  df-fo 6545  df-f1o 6546  df-fv 6547

This theorem is used by:  evlextv  34221