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

Theorem fvunsng 5580
Description: Remove an ordered pair not participating in a function value. (Contributed by Jim Kingdon, 7-Jan-2019.)
Assertion
Ref Expression
fvunsng ((𝐷𝑉𝐵𝐷) → ((𝐴 ∪ {⟨𝐵, 𝐶⟩})‘𝐷) = (𝐴𝐷))

Proof of Theorem fvunsng
StepHypRef Expression
1 snidg 3522 . . . 4 (𝐷𝑉𝐷 ∈ {𝐷})
2 fvres 5411 . . . 4 (𝐷 ∈ {𝐷} → (((𝐴 ∪ {⟨𝐵, 𝐶⟩}) ↾ {𝐷})‘𝐷) = ((𝐴 ∪ {⟨𝐵, 𝐶⟩})‘𝐷))
31, 2syl 14 . . 3 (𝐷𝑉 → (((𝐴 ∪ {⟨𝐵, 𝐶⟩}) ↾ {𝐷})‘𝐷) = ((𝐴 ∪ {⟨𝐵, 𝐶⟩})‘𝐷))
4 resundir 4801 . . . . 5 ((𝐴 ∪ {⟨𝐵, 𝐶⟩}) ↾ {𝐷}) = ((𝐴 ↾ {𝐷}) ∪ ({⟨𝐵, 𝐶⟩} ↾ {𝐷}))
5 elsni 3513 . . . . . . . . 9 (𝐵 ∈ {𝐷} → 𝐵 = 𝐷)
65necon3ai 2332 . . . . . . . 8 (𝐵𝐷 → ¬ 𝐵 ∈ {𝐷})
7 ressnop0 5567 . . . . . . . 8 𝐵 ∈ {𝐷} → ({⟨𝐵, 𝐶⟩} ↾ {𝐷}) = ∅)
86, 7syl 14 . . . . . . 7 (𝐵𝐷 → ({⟨𝐵, 𝐶⟩} ↾ {𝐷}) = ∅)
98uneq2d 3198 . . . . . 6 (𝐵𝐷 → ((𝐴 ↾ {𝐷}) ∪ ({⟨𝐵, 𝐶⟩} ↾ {𝐷})) = ((𝐴 ↾ {𝐷}) ∪ ∅))
10 un0 3364 . . . . . 6 ((𝐴 ↾ {𝐷}) ∪ ∅) = (𝐴 ↾ {𝐷})
119, 10syl6eq 2164 . . . . 5 (𝐵𝐷 → ((𝐴 ↾ {𝐷}) ∪ ({⟨𝐵, 𝐶⟩} ↾ {𝐷})) = (𝐴 ↾ {𝐷}))
124, 11syl5eq 2160 . . . 4 (𝐵𝐷 → ((𝐴 ∪ {⟨𝐵, 𝐶⟩}) ↾ {𝐷}) = (𝐴 ↾ {𝐷}))
1312fveq1d 5389 . . 3 (𝐵𝐷 → (((𝐴 ∪ {⟨𝐵, 𝐶⟩}) ↾ {𝐷})‘𝐷) = ((𝐴 ↾ {𝐷})‘𝐷))
143, 13sylan9req 2169 . 2 ((𝐷𝑉𝐵𝐷) → ((𝐴 ∪ {⟨𝐵, 𝐶⟩})‘𝐷) = ((𝐴 ↾ {𝐷})‘𝐷))
15 fvres 5411 . . . 4 (𝐷 ∈ {𝐷} → ((𝐴 ↾ {𝐷})‘𝐷) = (𝐴𝐷))
161, 15syl 14 . . 3 (𝐷𝑉 → ((𝐴 ↾ {𝐷})‘𝐷) = (𝐴𝐷))
1716adantr 272 . 2 ((𝐷𝑉𝐵𝐷) → ((𝐴 ↾ {𝐷})‘𝐷) = (𝐴𝐷))
1814, 17eqtrd 2148 1 ((𝐷𝑉𝐵𝐷) → ((𝐴 ∪ {⟨𝐵, 𝐶⟩})‘𝐷) = (𝐴𝐷))
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wa 103   = wceq 1314  wcel 1463  wne 2283  cun 3037  c0 3331  {csn 3495  cop 3498  cres 4509  cfv 5091
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 586  ax-in2 587  ax-io 681  ax-5 1406  ax-7 1407  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-8 1465  ax-10 1466  ax-11 1467  ax-i12 1468  ax-bndl 1469  ax-4 1470  ax-14 1475  ax-17 1489  ax-i9 1493  ax-ial 1497  ax-i5r 1498  ax-ext 2097  ax-sep 4014  ax-pow 4066  ax-pr 4099
This theorem depends on definitions:  df-bi 116  df-3an 947  df-tru 1317  df-fal 1320  df-nf 1420  df-sb 1719  df-clab 2102  df-cleq 2108  df-clel 2111  df-nfc 2245  df-ne 2284  df-ral 2396  df-rex 2397  df-v 2660  df-dif 3041  df-un 3043  df-in 3045  df-ss 3052  df-nul 3332  df-pw 3480  df-sn 3501  df-pr 3502  df-op 3504  df-uni 3705  df-br 3898  df-opab 3958  df-xp 4513  df-res 4519  df-iota 5056  df-fv 5099
This theorem is referenced by:  fvpr1  5590  fvpr1g  5592  fvpr2g  5593  fvtp1g  5594  tfrlemisucaccv  6188  tfr1onlemsucaccv  6204  tfrcllemsucaccv  6217  ac6sfi  6758  0tonninf  10152  1tonninf  10153  hashennn  10466  zfz1isolemiso  10522
  Copyright terms: Public domain W3C validator