Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  fvsnun2 Structured version   GIF version

Theorem fvsnun2 5286
 Description: The value of a function with one of its ordered pairs replaced, at arguments other than the replaced one. See also fvsnun1 5285. (Contributed by NM, 23-Sep-2007.)
Hypotheses
Ref Expression
fvsnun.1 A V
fvsnun.2 B V
fvsnun.3 𝐺 = ({⟨A, B⟩} ∪ (𝐹 ↾ (𝐶 ∖ {A})))
Assertion
Ref Expression
fvsnun2 (𝐷 (𝐶 ∖ {A}) → (𝐺𝐷) = (𝐹𝐷))

Proof of Theorem fvsnun2
StepHypRef Expression
1 fvsnun.3 . . . . 5 𝐺 = ({⟨A, B⟩} ∪ (𝐹 ↾ (𝐶 ∖ {A})))
21reseq1i 4535 . . . 4 (𝐺 ↾ (𝐶 ∖ {A})) = (({⟨A, B⟩} ∪ (𝐹 ↾ (𝐶 ∖ {A}))) ↾ (𝐶 ∖ {A}))
3 resundir 4553 . . . 4 (({⟨A, B⟩} ∪ (𝐹 ↾ (𝐶 ∖ {A}))) ↾ (𝐶 ∖ {A})) = (({⟨A, B⟩} ↾ (𝐶 ∖ {A})) ∪ ((𝐹 ↾ (𝐶 ∖ {A})) ↾ (𝐶 ∖ {A})))
4 disjdif 3273 . . . . . . 7 ({A} ∩ (𝐶 ∖ {A})) = ∅
5 fvsnun.1 . . . . . . . . 9 A V
6 fvsnun.2 . . . . . . . . 9 B V
75, 6fnsn 4879 . . . . . . . 8 {⟨A, B⟩} Fn {A}
8 fnresdisj 4935 . . . . . . . 8 ({⟨A, B⟩} Fn {A} → (({A} ∩ (𝐶 ∖ {A})) = ∅ ↔ ({⟨A, B⟩} ↾ (𝐶 ∖ {A})) = ∅))
97, 8ax-mp 7 . . . . . . 7 (({A} ∩ (𝐶 ∖ {A})) = ∅ ↔ ({⟨A, B⟩} ↾ (𝐶 ∖ {A})) = ∅)
104, 9mpbi 133 . . . . . 6 ({⟨A, B⟩} ↾ (𝐶 ∖ {A})) = ∅
11 residm 4569 . . . . . 6 ((𝐹 ↾ (𝐶 ∖ {A})) ↾ (𝐶 ∖ {A})) = (𝐹 ↾ (𝐶 ∖ {A}))
1210, 11uneq12i 3072 . . . . 5 (({⟨A, B⟩} ↾ (𝐶 ∖ {A})) ∪ ((𝐹 ↾ (𝐶 ∖ {A})) ↾ (𝐶 ∖ {A}))) = (∅ ∪ (𝐹 ↾ (𝐶 ∖ {A})))
13 uncom 3064 . . . . 5 (∅ ∪ (𝐹 ↾ (𝐶 ∖ {A}))) = ((𝐹 ↾ (𝐶 ∖ {A})) ∪ ∅)
14 un0 3228 . . . . 5 ((𝐹 ↾ (𝐶 ∖ {A})) ∪ ∅) = (𝐹 ↾ (𝐶 ∖ {A}))
1512, 13, 143eqtri 2046 . . . 4 (({⟨A, B⟩} ↾ (𝐶 ∖ {A})) ∪ ((𝐹 ↾ (𝐶 ∖ {A})) ↾ (𝐶 ∖ {A}))) = (𝐹 ↾ (𝐶 ∖ {A}))
162, 3, 153eqtri 2046 . . 3 (𝐺 ↾ (𝐶 ∖ {A})) = (𝐹 ↾ (𝐶 ∖ {A}))
1716fveq1i 5104 . 2 ((𝐺 ↾ (𝐶 ∖ {A}))‘𝐷) = ((𝐹 ↾ (𝐶 ∖ {A}))‘𝐷)
18 fvres 5123 . 2 (𝐷 (𝐶 ∖ {A}) → ((𝐺 ↾ (𝐶 ∖ {A}))‘𝐷) = (𝐺𝐷))
19 fvres 5123 . 2 (𝐷 (𝐶 ∖ {A}) → ((𝐹 ↾ (𝐶 ∖ {A}))‘𝐷) = (𝐹𝐷))
2017, 18, 193eqtr3a 2078 1 (𝐷 (𝐶 ∖ {A}) → (𝐺𝐷) = (𝐹𝐷))
 Colors of variables: wff set class Syntax hints:   → wi 4   ↔ wb 98   = wceq 1228   ∈ wcel 1374  Vcvv 2535   ∖ cdif 2891   ∪ cun 2892   ∩ cin 2893  ∅c0 3201  {csn 3350  ⟨cop 3353   ↾ cres 4274   Fn wfn 4824  ‘cfv 4829 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-in1 532  ax-in2 533  ax-io 617  ax-5 1316  ax-7 1317  ax-gen 1318  ax-ie1 1363  ax-ie2 1364  ax-8 1376  ax-10 1377  ax-11 1378  ax-i12 1379  ax-bnd 1380  ax-4 1381  ax-14 1386  ax-17 1400  ax-i9 1404  ax-ial 1409  ax-i5r 1410  ax-ext 2004  ax-sep 3849  ax-pow 3901  ax-pr 3918 This theorem depends on definitions:  df-bi 110  df-3an 875  df-tru 1231  df-fal 1234  df-nf 1330  df-sb 1628  df-eu 1885  df-mo 1886  df-clab 2009  df-cleq 2015  df-clel 2018  df-nfc 2149  df-ral 2289  df-rex 2290  df-v 2537  df-dif 2897  df-un 2899  df-in 2901  df-ss 2908  df-nul 3202  df-pw 3336  df-sn 3356  df-pr 3357  df-op 3359  df-uni 3555  df-br 3739  df-opab 3793  df-id 4004  df-xp 4278  df-rel 4279  df-cnv 4280  df-co 4281  df-dm 4282  df-res 4284  df-iota 4794  df-fun 4831  df-fn 4832  df-fv 4837 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator