Theorem fnsnfv 6964

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.

Step	Hyp	Ref	Expression
1		imasng 6081	. . 3 ⊢ (𝐵 ∈ 𝐴 → (𝐹 “ {𝐵}) = {𝑦 ∣ 𝐵𝐹𝑦})
2	1	adantl 487	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → (𝐹 “ {𝐵}) = {𝑦 ∣ 𝐵𝐹𝑦})
3		velsn 4599	. . . . 5 ⊢ (𝑦 ∈ {(𝐹‘𝐵)} ↔ 𝑦 = (𝐹‘𝐵))
4		eqcom 2767	. . . . 5 ⊢ (𝑦 = (𝐹‘𝐵) ↔ (𝐹‘𝐵) = 𝑦)
5	3, 4	bitri 278	. . . 4 ⊢ (𝑦 ∈ {(𝐹‘𝐵)} ↔ (𝐹‘𝐵) = 𝑦)
6		fnbrfvb 6935	. . . 4 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → ((𝐹‘𝐵) = 𝑦 ↔ 𝐵𝐹𝑦))
7	5, 6	bitr2id 287	. . 3 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → (𝐵𝐹𝑦 ↔ 𝑦 ∈ {(𝐹‘𝐵)}))
8	7	eqabcdv 2894	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → {𝑦 ∣ 𝐵𝐹𝑦} = {(𝐹‘𝐵)})
9	2, 8	eqtr2d 2796	1 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → {(𝐹‘𝐵)} = (𝐹 “ {𝐵}))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1569   ∈ wcel 2144  {cab 2738  {csn 4583   class class class wbr 5102   “ cima 5653   Fn wfn 6533  ‘cfv 6538

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-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 4584  df-pr 4586  df-op 4590  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 6540  df-fn 6541  df-fv 6546

This theorem is used by:  fnimapr  6968  fnimatpd  6969  funfv  6972  fvco2  6982  fvimacnvi  7051  fvimacnvALT  7056  fsn2  7137  fnimasnd  7373  fparlem3  8125  fparlem4  8126  suppval1  8183  suppsnop  8195  domunsncan  9096  phplem2  9220  domunfican  9313  fiint  9318  infdifsn  9658  cantnfp1lem3  9681  resunimafz0  14590  symgfixelsi  19649  dprdf1o  20248  frlmlbs  22103  f1lindf  22128  cnt1  23668  xkohaus  23972  xkoptsub  23973  ustuqtop3  24562  bday1  28200  old1  28251  madeoldsuc  28271  n0bday  28738  zcuts  28793  bdaypw2n0bndlem  28849  cyclnumvtx  30388  eulerpartlemmf  35007  poimirlem4  38543  poimirlem6  38545  poimirlem7  38546  poimirlem9  38548  poimirlem13  38552  poimirlem14  38553  poimirlem16  38555  poimirlem19  38558  grpokerinj  38828  k0004lem3  45149  funcoressn  48112  cycl3grtri  49045  imaf1homlem  50215