Metamath Proof Explorer

Theorem fvsnun2

Description: The value of a function with one of its ordered pairs replaced, at arguments other than the replaced one. See also fvsnun1 . (Contributed by NM, 23-Sep-2007) Put in deduction form. (Revised by BJ, 25-Feb-2023)

Ref Expression
Hypotheses fvsnun.1 ⊢ φ → A ∈ V
fvsnun.2 ⊢ φ → B ∈ W
fvsnun.3 ⊢ G = A B ∪ F ↾ C ∖ A
fvsnun2.4 ⊢ φ → D ∈ C ∖ A
Assertion fvsnun2 ⊢ φ → G ⁡ D = F ⁡ D

Proof

Step Hyp Ref Expression
1 fvsnun.1 ⊢ φ → A ∈ V
2 fvsnun.2 ⊢ φ → B ∈ W
3 fvsnun.3 ⊢ G = A B ∪ F ↾ C ∖ A
4 fvsnun2.4 ⊢ φ → D ∈ C ∖ A
5 3 reseq1i ⊢ G ↾ C ∖ A = A B ∪ F ↾ C ∖ A ↾ C ∖ A
6 5 a1i ⊢ φ → G ↾ C ∖ A = A B ∪ F ↾ C ∖ A ↾ C ∖ A
7 resundir ⊢ A B ∪ F ↾ C ∖ A ↾ C ∖ A = A B ↾ C ∖ A ∪ F ↾ C ∖ A ↾ C ∖ A
8 7 a1i ⊢ φ → A B ∪ F ↾ C ∖ A ↾ C ∖ A = A B ↾ C ∖ A ∪ F ↾ C ∖ A ↾ C ∖ A
9 disjdif ⊢ A ∩ C ∖ A = ∅
10 fnsng ⊢ A ∈ V ∧ B ∈ W → A B Fn A
11 1 2 10 syl2anc ⊢ φ → A B Fn A
12 fnresdisj ⊢ A B Fn A → A ∩ C ∖ A = ∅ ↔ A B ↾ C ∖ A = ∅
13 11 12 syl ⊢ φ → A ∩ C ∖ A = ∅ ↔ A B ↾ C ∖ A = ∅
14 9 13 mpbii ⊢ φ → A B ↾ C ∖ A = ∅
15 residm ⊢ F ↾ C ∖ A ↾ C ∖ A = F ↾ C ∖ A
16 15 a1i ⊢ φ → F ↾ C ∖ A ↾ C ∖ A = F ↾ C ∖ A
17 14 16 uneq12d ⊢ φ → A B ↾ C ∖ A ∪ F ↾ C ∖ A ↾ C ∖ A = ∅ ∪ F ↾ C ∖ A
18 uncom ⊢ ∅ ∪ F ↾ C ∖ A = F ↾ C ∖ A ∪ ∅
19 18 a1i ⊢ φ → ∅ ∪ F ↾ C ∖ A = F ↾ C ∖ A ∪ ∅
20 un0 ⊢ F ↾ C ∖ A ∪ ∅ = F ↾ C ∖ A
21 20 a1i ⊢ φ → F ↾ C ∖ A ∪ ∅ = F ↾ C ∖ A
22 17 19 21 3eqtrd ⊢ φ → A B ↾ C ∖ A ∪ F ↾ C ∖ A ↾ C ∖ A = F ↾ C ∖ A
23 6 8 22 3eqtrd ⊢ φ → G ↾ C ∖ A = F ↾ C ∖ A
24 23 fveq1d ⊢ φ → G ↾ C ∖ A ⁡ D = F ↾ C ∖ A ⁡ D
25 4 fvresd ⊢ φ → G ↾ C ∖ A ⁡ D = G ⁡ D
26 4 fvresd ⊢ φ → F ↾ C ∖ A ⁡ D = F ⁡ D
27 24 25 26 3eqtr3d ⊢ φ → G ⁡ D = F ⁡ D