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 3426 | . . 3 ⊢ (𝐵 ∈ 𝑉 → 𝐵 ∈ V) | |
2 | 1 | ralimi 3083 | . 2 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → ∀𝑥 ∈ 𝐴 𝐵 ∈ V) |
3 | mptfng.1 | . . 3 ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) | |
4 | 3 | mptfng 6517 | . 2 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ V ↔ 𝐹 Fn 𝐴) |
5 | 2, 4 | sylib 221 | 1 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → 𝐹 Fn 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1543 ∈ wcel 2110 ∀wral 3061 Vcvv 3408 ↦ cmpt 5135 Fn wfn 6375 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2158 ax-12 2175 ax-ext 2708 ax-sep 5192 ax-nul 5199 ax-pr 5322 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 848 df-3an 1091 df-tru 1546 df-fal 1556 df-ex 1788 df-nf 1792 df-sb 2071 df-mo 2539 df-eu 2568 df-clab 2715 df-cleq 2729 df-clel 2816 df-nfc 2886 df-ral 3066 df-rab 3070 df-v 3410 df-dif 3869 df-un 3871 df-in 3873 df-ss 3883 df-nul 4238 df-if 4440 df-sn 4542 df-pr 4544 df-op 4548 df-br 5054 df-opab 5116 df-mpt 5136 df-id 5455 df-xp 5557 df-rel 5558 df-cnv 5559 df-co 5560 df-dm 5561 df-fun 6382 df-fn 6383 |
This theorem is referenced by: fnmptd 6519 mpt0 6520 fnmptfvd 6861 ralrnmptw 6913 ralrnmpt 6915 fmpt 6927 fmpt2d 6940 f1ocnvd 7456 offval2 7488 ofrfval2 7489 fsplitfpar 7887 mptelixpg 8616 fifo 9048 cantnflem1 9304 infmap2 9832 compssiso 9988 gruiun 10413 mptnn0fsupp 13570 mptnn0fsuppr 13572 seqof 13633 rlimi2 15075 prdsbas3 16986 prdsbascl 16988 prdsdsval2 16989 quslem 17048 fnmrc 17110 isofn 17280 pmtrrn 18849 pmtrfrn 18850 pmtrdifwrdellem2 18874 gsummptcl 19352 mptscmfsupp0 19964 ofco2 21348 pmatcollpw2lem 21674 neif 21997 tgrest 22056 cmpfi 22305 elptr2 22471 xkoptsub 22551 ptcmplem2 22950 ptcmplem3 22951 prdsxmetlem 23266 prdsxmslem2 23427 bcth3 24228 uniioombllem6 24485 itg2const 24638 ellimc2 24774 dvrec 24852 dvmptres3 24853 ulmss 25289 ulmdvlem1 25292 ulmdvlem2 25293 ulmdvlem3 25294 itgulm2 25301 psercn 25318 tgjustr 26565 f1o3d 30681 f1od2 30776 psgnfzto1stlem 31086 frlmdim 31408 rmulccn 31592 esumnul 31728 esum0 31729 gsumesum 31739 ofcfval2 31784 signsplypnf 32241 signsply0 32242 hgt750lemb 32348 matunitlindflem1 35510 matunitlindflem2 35511 cdlemk56 38722 dicfnN 38934 hbtlem7 40653 refsumcn 42246 wessf1ornlem 42395 choicefi 42413 axccdom 42435 fsumsermpt 42795 liminfval2 42984 stoweidlem31 43247 stoweidlem59 43275 stirlinglem13 43302 dirkercncflem2 43320 fourierdlem62 43384 subsaliuncllem 43571 subsaliuncl 43572 hoidmvlelem3 43810 dfafn5b 44325 fundcmpsurinjlem2 44524 lincresunit2 45492 |
Copyright terms: Public domain | W3C validator |