Theorem fnsnfv 6961

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 6087	. . 3 ⊢ (𝐵 ∈ 𝐴 → (𝐹 “ {𝐵}) = {𝑦 ∣ 𝐵𝐹𝑦})
2	1	adantl 486	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → (𝐹 “ {𝐵}) = {𝑦 ∣ 𝐵𝐹𝑦})
3		velsn 4608	. . . . 5 ⊢ (𝑦 ∈ {(𝐹‘𝐵)} ↔ 𝑦 = (𝐹‘𝐵))
4		eqcom 2776	. . . . 5 ⊢ (𝑦 = (𝐹‘𝐵) ↔ (𝐹‘𝐵) = 𝑦)
5	3, 4	bitri 278	. . . 4 ⊢ (𝑦 ∈ {(𝐹‘𝐵)} ↔ (𝐹‘𝐵) = 𝑦)
6		fnbrfvb 6932	. . . 4 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → ((𝐹‘𝐵) = 𝑦 ↔ 𝐵𝐹𝑦))
7	5, 6	bitr2id 287	. . 3 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → (𝐵𝐹𝑦 ↔ 𝑦 ∈ {(𝐹‘𝐵)}))
8	7	eqabcdv 2903	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → {𝑦 ∣ 𝐵𝐹𝑦} = {(𝐹‘𝐵)})
9	2, 8	eqtr2d 2805	1 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → {(𝐹‘𝐵)} = (𝐹 “ {𝐵}))

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1567   ∈ wcel 2149  {cab 2747  {csn 4592   class class class wbr 5111   “ cima 5665   Fn wfn 6532  ‘cfv 6537

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-12 2219  ax-ext 2741  ax-sep 5259  ax-nul 5271  ax-pr 5405

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-ne 2965  df-ral 3086  df-rex 3096  df-rab 3423  df-v 3463  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4293  df-if 4491  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5112  df-opab 5176  df-id 5557  df-xp 5668  df-rel 5669  df-cnv 5670  df-co 5671  df-dm 5672  df-rn 5673  df-res 5674  df-ima 5675  df-iota 6493  df-fun 6539  df-fn 6540  df-fv 6545

This theorem is referenced by:  fnimapr  6965  fnimatpd  6966  funfv  6969  fvco2  6979  fvimacnvi  7048  fvimacnvALT  7053  fsn2  7133  fnimasnd  7364  fparlem3  8109  fparlem4  8110  suppval1  8162  suppsnop  8174  domunsncan  9065  phplem2  9189  domunfican  9281  fiint  9286  infdifsn  9626  cantnfp1lem3  9649  resunimafz0  14482  symgfixelsi  19505  dprdf1o  20104  frlmlbs  21916  f1lindf  21941  cnt1  23476  xkohaus  23779  xkoptsub  23780  ustuqtop3  24369  bday1  27973  old1  28024  madeoldsuc  28044  n0bday  28511  zcuts  28566  bdaypw2n0bndlem  28622  cyclnumvtx  30090  eulerpartlemmf  34710  poimirlem4  38198  poimirlem6  38200  poimirlem7  38201  poimirlem9  38203  poimirlem13  38207  poimirlem14  38208  poimirlem16  38210  poimirlem19  38213  grpokerinj  38467  k0004lem3  44802  funcoressn  47703  cycl3grtri  48636  imaf1homlem  49805