![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > fnsnfv | Structured version Visualization version GIF version |
Description: Singleton of function value. (Contributed by NM, 22-May-1998.) |
Ref | Expression |
---|---|
fnsnfv | ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → {(𝐹‘𝐵)} = (𝐹 “ {𝐵})) |
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 𝐴 ∧ 𝐵 ∈ 𝐴) → {(𝐹‘𝐵)} = (𝐹 “ {𝐵})) |
Colors of variables: wff setvar class |
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 |
Copyright terms: Public domain | W3C validator |