![]() |
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 3509 | . . 3 ⊢ (𝐵 ∈ 𝑉 → 𝐵 ∈ V) | |
2 | 1 | ralimi 3089 | . 2 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → ∀𝑥 ∈ 𝐴 𝐵 ∈ V) |
3 | mptfng.1 | . . 3 ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) | |
4 | 3 | mptfng 6719 | . 2 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ V ↔ 𝐹 Fn 𝐴) |
5 | 2, 4 | sylib 218 | 1 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → 𝐹 Fn 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1537 ∈ wcel 2108 ∀wral 3067 Vcvv 3488 ↦ cmpt 5249 Fn wfn 6568 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1793 ax-4 1807 ax-5 1909 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2158 ax-12 2178 ax-ext 2711 ax-sep 5317 ax-nul 5324 ax-pr 5447 |
This theorem depends on definitions: df-bi 207 df-an 396 df-or 847 df-3an 1089 df-tru 1540 df-fal 1550 df-ex 1778 df-nf 1782 df-sb 2065 df-mo 2543 df-eu 2572 df-clab 2718 df-cleq 2732 df-clel 2819 df-nfc 2895 df-ral 3068 df-rex 3077 df-rab 3444 df-v 3490 df-dif 3979 df-un 3981 df-ss 3993 df-nul 4353 df-if 4549 df-sn 4649 df-pr 4651 df-op 4655 df-br 5167 df-opab 5229 df-mpt 5250 df-id 5593 df-xp 5706 df-rel 5707 df-cnv 5708 df-co 5709 df-dm 5710 df-fun 6575 df-fn 6576 |
This theorem is referenced by: fnmptd 6721 mpt0 6722 fnmptfvd 7074 ralrnmptw 7128 ralrnmpt 7130 fmpt 7144 fmpt2d 7158 f1ocnvd 7701 offval2 7734 ofrfval2 7735 mptcnfimad 8027 fsplitfpar 8159 mptelixpg 8993 fifo 9501 cantnflem1 9758 infmap2 10286 compssiso 10443 gruiun 10868 mptnn0fsupp 14048 mptnn0fsuppr 14050 seqof 14110 rlimi2 15560 prdsbas3 17541 prdsbascl 17543 prdsdsval2 17544 quslem 17603 fnmrc 17665 isofn 17836 ghmquskerco 19324 pmtrrn 19499 pmtrfrn 19500 pmtrdifwrdellem2 19524 gsummptcl 20009 mptscmfsupp0 20947 ofco2 22478 pmatcollpw2lem 22804 neif 23129 tgrest 23188 cmpfi 23437 elptr2 23603 xkoptsub 23683 ptcmplem2 24082 ptcmplem3 24083 prdsxmetlem 24399 prdsxmslem2 24563 bcth3 25384 uniioombllem6 25642 itg2const 25795 ellimc2 25932 dvrec 26013 dvmptres3 26014 ulmss 26458 ulmdvlem1 26461 ulmdvlem2 26462 ulmdvlem3 26463 itgulm2 26470 psercn 26488 tgjustr 28500 f1o3d 32646 f1od2 32735 psgnfzto1stlem 33093 frlmdim 33624 rmulccn 33874 esumnul 34012 esum0 34013 gsumesum 34023 ofcfval2 34068 signsplypnf 34527 signsply0 34528 hgt750lemb 34633 wevgblacfn 35076 matunitlindflem1 37576 matunitlindflem2 37577 cdlemk56 40928 dicfnN 41140 hbtlem7 43082 refsumcn 44930 wessf1ornlem 45092 choicefi 45107 axccdom 45129 fsumsermpt 45500 liminfval2 45689 stoweidlem31 45952 stoweidlem59 45980 stirlinglem13 46007 dirkercncflem2 46025 fourierdlem62 46089 subsaliuncllem 46278 subsaliuncl 46279 hoidmvlelem3 46518 dfafn5b 47076 fundcmpsurinjlem2 47273 lincresunit2 48207 |
Copyright terms: Public domain | W3C validator |