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 3212 | . . 3 ⊢ (𝐵 ∈ 𝑉 → 𝐵 ∈ V) | |
2 | 1 | ralimi 2952 | . 2 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → ∀𝑥 ∈ 𝐴 𝐵 ∈ V) |
3 | mptfng.1 | . . 3 ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) | |
4 | 3 | mptfng 6019 | . 2 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ V ↔ 𝐹 Fn 𝐴) |
5 | 2, 4 | sylib 208 | 1 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → 𝐹 Fn 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1483 ∈ wcel 1990 ∀wral 2912 Vcvv 3200 ↦ cmpt 4729 Fn wfn 5883 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-sep 4781 ax-nul 4789 ax-pr 4906 |
This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3an 1039 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ral 2917 df-rab 2921 df-v 3202 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-nul 3916 df-if 4087 df-sn 4178 df-pr 4180 df-op 4184 df-br 4654 df-opab 4713 df-mpt 4730 df-id 5024 df-xp 5120 df-rel 5121 df-cnv 5122 df-co 5123 df-dm 5124 df-fun 5890 df-fn 5891 |
This theorem is referenced by: mpt0 6021 fnmptfvd 6320 ralrnmpt 6368 fmpt 6381 fmpt2d 6393 f1ocnvd 6884 offval2 6914 ofrfval2 6915 mptelixpg 7945 fifo 8338 cantnflem1 8586 infmap2 9040 compssiso 9196 gruiun 9621 mptnn0fsupp 12797 mptnn0fsuppr 12799 seqof 12858 rlimi2 14245 prdsbas3 16141 prdsbascl 16143 prdsdsval2 16144 quslem 16203 fnmrc 16267 isofn 16435 pmtrrn 17877 pmtrfrn 17878 pmtrdifwrdellem2 17902 gsummptcl 18366 mptscmfsupp0 18928 ofco2 20257 pmatcollpw2lem 20582 neif 20904 tgrest 20963 cmpfi 21211 elptr2 21377 xkoptsub 21457 ptcmplem2 21857 ptcmplem3 21858 prdsxmetlem 22173 prdsxmslem2 22334 bcth3 23128 uniioombllem6 23356 itg2const 23507 ellimc2 23641 dvrec 23718 dvmptres3 23719 ulmss 24151 ulmdvlem1 24154 ulmdvlem2 24155 ulmdvlem3 24156 itgulm2 24163 psercn 24180 f1o3d 29431 f1od2 29499 psgnfzto1stlem 29850 rmulccn 29974 esumnul 30110 esum0 30111 gsumesum 30121 ofcfval2 30166 signsplypnf 30627 signsply0 30628 hgt750lemb 30734 matunitlindflem1 33405 matunitlindflem2 33406 cdlemk56 36259 dicfnN 36472 hbtlem7 37695 refsumcn 39189 wessf1ornlem 39371 choicefi 39392 axccdom 39416 fnmptd 39434 fsumsermpt 39811 liminfval2 40000 stoweidlem31 40248 stoweidlem59 40276 stirlinglem13 40303 dirkercncflem2 40321 fourierdlem62 40385 subsaliuncllem 40575 subsaliuncl 40576 hoidmvlelem3 40811 dfafn5b 41241 lincresunit2 42267 |
Copyright terms: Public domain | W3C validator |