![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > fnmpt | Structured version Visualization version Unicode version |
Description: The maps-to notation defines a function with domain. (Contributed by NM, 9-Apr-2013.) |
Ref | Expression |
---|---|
mptfng.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
fnmpt |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elex 3040 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | ralimi 2796 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | mptfng.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 3 | mptfng 5713 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | 2, 4 | sylib 201 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1677 ax-4 1690 ax-5 1766 ax-6 1813 ax-7 1859 ax-9 1913 ax-10 1932 ax-11 1937 ax-12 1950 ax-13 2104 ax-ext 2451 ax-sep 4518 ax-nul 4527 ax-pr 4639 |
This theorem depends on definitions: df-bi 190 df-or 377 df-an 378 df-3an 1009 df-tru 1455 df-ex 1672 df-nf 1676 df-sb 1806 df-eu 2323 df-mo 2324 df-clab 2458 df-cleq 2464 df-clel 2467 df-nfc 2601 df-ne 2643 df-ral 2761 df-rex 2762 df-rab 2765 df-v 3033 df-dif 3393 df-un 3395 df-in 3397 df-ss 3404 df-nul 3723 df-if 3873 df-sn 3960 df-pr 3962 df-op 3966 df-br 4396 df-opab 4455 df-mpt 4456 df-id 4754 df-xp 4845 df-rel 4846 df-cnv 4847 df-co 4848 df-dm 4849 df-fun 5591 df-fn 5592 |
This theorem is referenced by: mpt0 5715 fnmptfvd 6000 ralrnmpt 6046 fmpt 6058 fmpt2d 6069 f1ocnvd 6537 offval2 6567 ofrfval2 6568 mptelixpg 7577 fifo 7964 cantnflem1 8212 infmap2 8666 compssiso 8822 gruiun 9242 mptnn0fsupp 12247 mptnn0fsuppr 12249 seqof 12308 rlimi2 13655 prdsbas3 15457 prdsbascl 15459 prdsdsval2 15460 quslem 15527 fnmrc 15591 isofn 15758 pmtrrn 17176 pmtrfrn 17177 pmtrdifwrdellem2 17201 gsummptcl 17677 dprdwdOLD 17722 mptscmfsupp0 18231 ofco2 19553 pmatcollpw2lem 19878 neif 20193 tgrest 20252 cmpfi 20500 elptr2 20666 xkoptsub 20746 ptcmplem2 21146 ptcmplem3 21147 prdsxmetlem 21461 prdsxmslem2 21622 bcth3 22377 uniioombllem6 22625 itg2const 22777 ellimc2 22911 dvrec 22988 dvmptres3 22989 ulmss 23431 ulmdvlem1 23434 ulmdvlem2 23435 ulmdvlem3 23436 itgulm2 23443 psercn 23460 f1o3d 28305 f1od2 28384 psgnfzto1stlem 28687 rmulccn 28808 esumnul 28943 esum0 28944 gsumesum 28954 ofcfval2 28999 signsplypnf 29511 signsply0 29512 cdlemk56 34609 dicfnN 34822 hbtlem7 36055 refsumcn 37414 wessf1ornlem 37530 choicefi 37552 fsumsermpt 37754 stoweidlem31 38004 stoweidlem59 38032 stirlinglem13 38060 dirkercncflem2 38078 fourierdlem62 38144 hoidmvlelem3 38537 dfafn5b 38808 lincresunit2 40779 |
Copyright terms: Public domain | W3C validator |