Theorem fnsnfv 6615

Description: Singleton of function value. (Contributed by NM, 22-May-1998.)

Assertion

Ref	Expression
fnsnfv	⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → {(𝐹‘𝐵)} = (𝐹 “ {𝐵}))

Proof of Theorem fnsnfv

Dummy variable 𝑦 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqcom 2802	. . . 4 ⊢ (𝑦 = (𝐹‘𝐵) ↔ (𝐹‘𝐵) = 𝑦)
2		fnbrfvb 6591	. . . 4 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → ((𝐹‘𝐵) = 𝑦 ↔ 𝐵𝐹𝑦))
3	1, 2	syl5bb 284	. . 3 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → (𝑦 = (𝐹‘𝐵) ↔ 𝐵𝐹𝑦))
4	3	abbidv 2860	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → {𝑦 ∣ 𝑦 = (𝐹‘𝐵)} = {𝑦 ∣ 𝐵𝐹𝑦})
5		df-sn 4477	. . 3 ⊢ {(𝐹‘𝐵)} = {𝑦 ∣ 𝑦 = (𝐹‘𝐵)}
6	5	a1i 11	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → {(𝐹‘𝐵)} = {𝑦 ∣ 𝑦 = (𝐹‘𝐵)})
7		fnrel 6329	. . . 4 ⊢ (𝐹 Fn 𝐴 → Rel 𝐹)
8		relimasn 5833	. . . 4 ⊢ (Rel 𝐹 → (𝐹 “ {𝐵}) = {𝑦 ∣ 𝐵𝐹𝑦})
9	7, 8	syl 17	. . 3 ⊢ (𝐹 Fn 𝐴 → (𝐹 “ {𝐵}) = {𝑦 ∣ 𝐵𝐹𝑦})
10	9	adantr 481	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → (𝐹 “ {𝐵}) = {𝑦 ∣ 𝐵𝐹𝑦})
11	4, 6, 10	3eqtr4d 2841	1 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → {(𝐹‘𝐵)} = (𝐹 “ {𝐵}))

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1522   ∈ wcel 2081  {cab 2775  {csn 4476   class class class wbr 4966   “ cima 5451  Rel wrel 5453   Fn wfn 6225  ‘cfv 6230

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-13 2344  ax-ext 2769  ax-sep 5099  ax-nul 5106  ax-pr 5226

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3an 1082  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-mo 2576  df-eu 2612  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-ne 2985  df-ral 3110  df-rex 3111  df-rab 3114  df-v 3439  df-sbc 3710  df-dif 3866  df-un 3868  df-in 3870  df-ss 3878  df-nul 4216  df-if 4386  df-sn 4477  df-pr 4479  df-op 4483  df-uni 4750  df-br 4967  df-opab 5029  df-id 5353  df-xp 5454  df-rel 5455  df-cnv 5456  df-co 5457  df-dm 5458  df-rn 5459  df-res 5460  df-ima 5461  df-iota 6194  df-fun 6232  df-fn 6233  df-fv 6238

This theorem is referenced by:  fnimapr  6619  funfv  6622  fvco2  6630  fvimacnvi  6692  fvimacnvALT  6697  fsn2  6766  fparlem3  7670  fparlem4  7671  suppval1  7692  suppsnop  7700  domunsncan  8469  phplem4  8551  domunfican  8642  fiint  8646  infdifsn  8971  cantnfp1lem3  8994  resunimafz0  13656  symgfixelsi  18299  dprdf1o  18876  frlmlbs  20628  f1lindf  20653  cnt1  21647  xkohaus  21950  xkoptsub  21951  ustuqtop3  22540  fnimatp  30118  eulerpartlemmf  31255  poimirlem4  34452  poimirlem6  34454  poimirlem7  34455  poimirlem9  34457  poimirlem13  34461  poimirlem14  34462  poimirlem16  34464  poimirlem19  34467  grpokerinj  34728  k0004lem3  40009  funcoressn  42819