Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > fnmpti | Structured version Visualization version GIF version |
Description: Functionality and domain of an ordered-pair class abstraction. (Contributed by NM, 29-Jan-2004.) (Revised by Mario Carneiro, 31-Aug-2015.) |
Ref | Expression |
---|---|
fnmpti.1 | ⊢ 𝐵 ∈ V |
fnmpti.2 | ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) |
Ref | Expression |
---|---|
fnmpti | ⊢ 𝐹 Fn 𝐴 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fnmpti.1 | . . 3 ⊢ 𝐵 ∈ V | |
2 | 1 | rgenw 2908 | . 2 ⊢ ∀𝑥 ∈ 𝐴 𝐵 ∈ V |
3 | fnmpti.2 | . . 3 ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) | |
4 | 3 | mptfng 5932 | . 2 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ V ↔ 𝐹 Fn 𝐴) |
5 | 2, 4 | mpbi 219 | 1 ⊢ 𝐹 Fn 𝐴 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1475 ∈ wcel 1977 ∀wral 2896 Vcvv 3173 ↦ cmpt 4643 Fn wfn 5799 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-9 1986 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 ax-sep 4709 ax-nul 4717 ax-pr 4833 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-3an 1033 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-eu 2462 df-mo 2463 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-ral 2901 df-rab 2905 df-v 3175 df-dif 3543 df-un 3545 df-in 3547 df-ss 3554 df-nul 3875 df-if 4037 df-sn 4126 df-pr 4128 df-op 4132 df-br 4584 df-opab 4644 df-mpt 4645 df-id 4953 df-xp 5044 df-rel 5045 df-cnv 5046 df-co 5047 df-dm 5048 df-fun 5806 df-fn 5807 |
This theorem is referenced by: dmmpti 5936 fconst 6004 dffn5 6151 eufnfv 6395 idref 6403 offn 6806 caofinvl 6822 fo1st 7079 fo2nd 7080 reldm 7110 mapsnf1o2 7791 unfilem2 8110 fidomdm 8128 pwfilem 8143 noinfep 8440 aceq3lem 8826 dfac4 8828 ackbij2lem2 8945 cfslb2n 8973 axcc2lem 9141 konigthlem 9269 rankcf 9478 tskuni 9484 seqf1o 12704 ccatlen 13213 ccatvalfn 13218 swrdlen 13275 swrdswrd 13312 sqrtf 13951 mptfzshft 14352 fsumrev 14353 fprodrev 14546 efcvgfsum 14655 prmreclem2 15459 1arith 15469 vdwlem6 15528 vdwlem8 15530 slotfn 15709 topnfn 15909 fnmre 16074 cidffn 16162 cidfn 16163 funcres 16379 yonedainv 16744 fn0g 17085 grpinvfn 17285 conjnmz 17517 psgnfn 17744 odf 17779 sylow1lem4 17839 pgpssslw 17852 sylow2blem3 17860 sylow3lem2 17866 cygctb 18116 dprd2da 18264 fnmgp 18314 rlmfn 19011 rrgsupp 19112 asclfn 19157 evlslem1 19336 frlmup4 19959 mdetrlin 20227 fncld 20636 hauseqlcld 21259 kqf 21360 filunirn 21496 fmf 21559 txflf 21620 clsnsg 21723 tgpconcomp 21726 qustgpopn 21733 qustgplem 21734 ustfn 21815 xmetunirn 21952 met1stc 22136 rrxmvallem 22995 ovolf 23057 vitali 23188 i1fmulc 23276 mbfi1fseqlem4 23291 itg2seq 23315 itg2monolem1 23323 i1fibl 23380 fncpn 23502 lhop1lem 23580 mdegxrf 23632 aannenlem3 23889 efabl 24100 logccv 24209 gausslemma2dlem1 24891 padicabvf 25120 mptelee 25575 wlkiswwlk2lem1 26219 clwlkisclwwlklem2a2 26308 grpoinvf 26770 occllem 27546 pjfni 27944 pjmfn 27958 rnbra 28350 bra11 28351 kbass2 28360 hmopidmchi 28394 xppreima2 28830 abfmpunirn 28832 dmct 28877 psgnfzto1stlem 29181 fimaproj 29228 locfinreflem 29235 ofcfn 29489 sxbrsigalem3 29661 eulerpartgbij 29761 sseqfv1 29778 sseqfn 29779 sseqf 29781 sseqfv2 29783 signstlen 29970 msubrn 30680 msrf 30693 faclimlem1 30882 matunitlindflem1 32575 poimirlem30 32609 mblfinlem2 32617 volsupnfl 32624 cnambfre 32628 itg2addnclem2 32632 itg2addnclem3 32633 ftc1anclem5 32659 ftc1anclem7 32661 sdclem2 32708 prdsbnd2 32764 rrncmslem 32801 diafn 35341 cdlemm10N 35425 dibfna 35461 lcfrlem9 35857 mapd1o 35955 hdmapfnN 36139 hgmapfnN 36198 rmxypairf1o 36494 hbtlem6 36718 dgraaf 36736 cytpfn 36805 ntrf 37441 uzmptshftfval 37567 binomcxplemrat 37571 addrfn 37697 subrfn 37698 mulvfn 37699 fourierdlem62 39061 fourierdlem70 39069 fourierdlem71 39070 fmtnorn 39984 1wlkiswwlks2lem1 41066 clwlkclwwlklem2a2 41202 zrinitorngc 41792 zrtermorngc 41793 zrtermoringc 41862 |
Copyright terms: Public domain | W3C validator |