MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  fnsnfv Structured version   Visualization version   GIF version

Theorem fnsnfv 6971
Description: Singleton of function value. (Contributed by NM, 22-May-1998.) (Proof shortened by Scott Fenton, 8-Aug-2024.)
Assertion
Ref Expression
fnsnfv ((𝐹 Fn 𝐴𝐵𝐴) → {(𝐹𝐵)} = (𝐹 “ {𝐵}))

Proof of Theorem fnsnfv
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 imasng 6083 . . 3 (𝐵𝐴 → (𝐹 “ {𝐵}) = {𝑦𝐵𝐹𝑦})
21adantl 480 . 2 ((𝐹 Fn 𝐴𝐵𝐴) → (𝐹 “ {𝐵}) = {𝑦𝐵𝐹𝑦})
3 velsn 4645 . . . . 5 (𝑦 ∈ {(𝐹𝐵)} ↔ 𝑦 = (𝐹𝐵))
4 eqcom 2737 . . . . 5 (𝑦 = (𝐹𝐵) ↔ (𝐹𝐵) = 𝑦)
53, 4bitri 274 . . . 4 (𝑦 ∈ {(𝐹𝐵)} ↔ (𝐹𝐵) = 𝑦)
6 fnbrfvb 6945 . . . 4 ((𝐹 Fn 𝐴𝐵𝐴) → ((𝐹𝐵) = 𝑦𝐵𝐹𝑦))
75, 6bitr2id 283 . . 3 ((𝐹 Fn 𝐴𝐵𝐴) → (𝐵𝐹𝑦𝑦 ∈ {(𝐹𝐵)}))
87eqabcdv 2866 . 2 ((𝐹 Fn 𝐴𝐵𝐴) → {𝑦𝐵𝐹𝑦} = {(𝐹𝐵)})
92, 8eqtr2d 2771 1 ((𝐹 Fn 𝐴𝐵𝐴) → {(𝐹𝐵)} = (𝐹 “ {𝐵}))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 394   = wceq 1539  wcel 2104  {cab 2707  {csn 4629   class class class wbr 5149  cima 5680   Fn wfn 6539  cfv 6544
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-12 2169  ax-ext 2701  ax-sep 5300  ax-nul 5307  ax-pr 5428
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-ne 2939  df-ral 3060  df-rex 3069  df-rab 3431  df-v 3474  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-opab 5212  df-id 5575  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-iota 6496  df-fun 6546  df-fn 6547  df-fv 6552
This theorem is referenced by:  fnimapr  6976  funfv  6979  fvco2  6989  fvimacnvi  7054  fvimacnvALT  7059  fsn2  7137  fparlem3  8104  fparlem4  8105  suppval1  8156  suppsnop  8167  domunsncan  9076  imafi  9179  phplem2  9212  phplem4OLD  9224  domunfican  9324  fiint  9328  infdifsn  9656  cantnfp1lem3  9679  resunimafz0  14410  symgfixelsi  19346  dprdf1o  19945  frlmlbs  21573  f1lindf  21598  cnt1  23076  xkohaus  23379  xkoptsub  23380  ustuqtop3  23970  bday1s  27567  old1  27605  madeoldsuc  27614  fnimatp  32167  eulerpartlemmf  33670  poimirlem4  36797  poimirlem6  36799  poimirlem7  36800  poimirlem9  36802  poimirlem13  36806  poimirlem14  36807  poimirlem16  36809  poimirlem19  36812  grpokerinj  37066  fnimasnd  41360  k0004lem3  43204  funcoressn  46052
  Copyright terms: Public domain W3C validator