![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > fnmpt | Structured version Visualization version GIF version |
Description: The maps-to notation defines a function with domain. (Contributed by NM, 9-Apr-2013.) |
Ref | Expression |
---|---|
mptfng.1 | ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) |
Ref | Expression |
---|---|
fnmpt | ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → 𝐹 Fn 𝐴) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elex 3462 | . . 3 ⊢ (𝐵 ∈ 𝑉 → 𝐵 ∈ V) | |
2 | 1 | ralimi 3085 | . 2 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → ∀𝑥 ∈ 𝐴 𝐵 ∈ V) |
3 | mptfng.1 | . . 3 ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) | |
4 | 3 | mptfng 6636 | . 2 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ V ↔ 𝐹 Fn 𝐴) |
5 | 2, 4 | sylib 217 | 1 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → 𝐹 Fn 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1542 ∈ wcel 2107 ∀wral 3063 Vcvv 3444 ↦ cmpt 5187 Fn wfn 6487 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-10 2138 ax-11 2155 ax-12 2172 ax-ext 2709 ax-sep 5255 ax-nul 5262 ax-pr 5383 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-nf 1787 df-sb 2069 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2816 df-nfc 2888 df-ral 3064 df-rex 3073 df-rab 3407 df-v 3446 df-dif 3912 df-un 3914 df-in 3916 df-ss 3926 df-nul 4282 df-if 4486 df-sn 4586 df-pr 4588 df-op 4592 df-br 5105 df-opab 5167 df-mpt 5188 df-id 5529 df-xp 5637 df-rel 5638 df-cnv 5639 df-co 5640 df-dm 5641 df-fun 6494 df-fn 6495 |
This theorem is referenced by: fnmptd 6638 mpt0 6639 fnmptfvd 6987 ralrnmptw 7039 ralrnmpt 7041 fmpt 7053 fmpt2d 7066 f1ocnvd 7595 offval2 7628 ofrfval2 7629 fsplitfpar 8039 mptelixpg 8807 fifo 9302 cantnflem1 9559 infmap2 10088 compssiso 10244 gruiun 10669 mptnn0fsupp 13832 mptnn0fsuppr 13834 seqof 13895 rlimi2 15332 prdsbas3 17299 prdsbascl 17301 prdsdsval2 17302 quslem 17361 fnmrc 17423 isofn 17594 pmtrrn 19174 pmtrfrn 19175 pmtrdifwrdellem2 19199 gsummptcl 19679 mptscmfsupp0 20316 ofco2 21728 pmatcollpw2lem 22054 neif 22379 tgrest 22438 cmpfi 22687 elptr2 22853 xkoptsub 22933 ptcmplem2 23332 ptcmplem3 23333 prdsxmetlem 23649 prdsxmslem2 23813 bcth3 24623 uniioombllem6 24880 itg2const 25033 ellimc2 25169 dvrec 25247 dvmptres3 25248 ulmss 25684 ulmdvlem1 25687 ulmdvlem2 25688 ulmdvlem3 25689 itgulm2 25696 psercn 25713 tgjustr 27221 f1o3d 31345 f1od2 31439 psgnfzto1stlem 31750 frlmdim 32098 rmulccn 32289 esumnul 32427 esum0 32428 gsumesum 32438 ofcfval2 32483 signsplypnf 32942 signsply0 32943 hgt750lemb 33049 matunitlindflem1 36005 matunitlindflem2 36006 cdlemk56 39365 dicfnN 39577 hbtlem7 41354 refsumcn 43036 wessf1ornlem 43198 choicefi 43216 axccdom 43238 fsumsermpt 43611 liminfval2 43800 stoweidlem31 44063 stoweidlem59 44091 stirlinglem13 44118 dirkercncflem2 44136 fourierdlem62 44200 subsaliuncllem 44389 subsaliuncl 44390 hoidmvlelem3 44629 dfafn5b 45184 fundcmpsurinjlem2 45382 lincresunit2 46350 |
Copyright terms: Public domain | W3C validator |