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 2924 | . 2 ⊢ ∀𝑥 ∈ 𝐴 𝐵 ∈ V |
3 | fnmpti.2 | . . 3 ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) | |
4 | 3 | mptfng 6019 | . 2 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ V ↔ 𝐹 Fn 𝐴) |
5 | 2, 4 | mpbi 220 | 1 ⊢ 𝐹 Fn 𝐴 |
Colors of variables: wff setvar class |
Syntax hints: = 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: dmmpti 6023 fconst 6091 dffn5 6241 eufnfv 6491 idref 6499 offn 6908 caofinvl 6924 fo1st 7188 fo2nd 7189 reldm 7219 mapsnf1o2 7905 unfilem2 8225 fidomdm 8243 pwfilem 8260 noinfep 8557 aceq3lem 8943 dfac4 8945 ackbij2lem2 9062 cfslb2n 9090 axcc2lem 9258 dmct 9346 konigthlem 9390 rankcf 9599 tskuni 9605 seqf1o 12842 ccatlen 13360 ccatvalfn 13365 swrdlen 13423 swrdswrd 13460 sqrtf 14103 mptfzshft 14510 fsumrev 14511 fprodrev 14707 efcvgfsum 14816 prmreclem2 15621 1arith 15631 vdwlem6 15690 vdwlem8 15692 slotfn 15875 topnfn 16086 fnmre 16251 cidffn 16339 cidfn 16340 funcres 16556 yonedainv 16921 fn0g 17262 grpinvfn 17462 conjnmz 17694 psgnfn 17921 odf 17956 sylow1lem4 18016 pgpssslw 18029 sylow2blem3 18037 sylow3lem2 18043 cygctb 18293 dprd2da 18441 fnmgp 18491 rlmfn 19190 rrgsupp 19291 asclfn 19336 evlslem1 19515 frlmup4 20140 mdetrlin 20408 fncld 20826 hauseqlcld 21449 kqf 21550 filunirn 21686 fmf 21749 txflf 21810 clsnsg 21913 tgpconncomp 21916 qustgpopn 21923 qustgplem 21924 ustfn 22005 xmetunirn 22142 met1stc 22326 rrxmvallem 23187 ovolf 23250 vitali 23382 i1fmulc 23470 mbfi1fseqlem4 23485 itg2seq 23509 itg2monolem1 23517 i1fibl 23574 fncpn 23696 lhop1lem 23776 mdegxrf 23828 aannenlem3 24085 efabl 24296 logccv 24409 gausslemma2dlem1 25091 padicabvf 25320 mptelee 25775 wlkiswwlks2lem1 26755 clwlkclwwlklem2a2 26894 grpoinvf 27386 occllem 28162 pjfni 28560 pjmfn 28574 rnbra 28966 bra11 28967 kbass2 28976 hmopidmchi 29010 xppreima2 29450 abfmpunirn 29452 psgnfzto1stlem 29850 fimaproj 29900 locfinreflem 29907 ofcfn 30162 sxbrsigalem3 30334 eulerpartgbij 30434 sseqfv1 30451 sseqfn 30452 sseqf 30454 sseqfv2 30456 signstlen 30644 msubrn 31426 msrf 31439 faclimlem1 31629 bj-evalfn 33026 matunitlindflem1 33405 poimirlem30 33439 mblfinlem2 33447 volsupnfl 33454 cnambfre 33458 itg2addnclem2 33462 itg2addnclem3 33463 ftc1anclem5 33489 ftc1anclem7 33491 sdclem2 33538 prdsbnd2 33594 rrncmslem 33631 diafn 36323 cdlemm10N 36407 dibfna 36443 lcfrlem9 36839 mapd1o 36937 hdmapfnN 37121 hgmapfnN 37180 rmxypairf1o 37476 hbtlem6 37699 dgraaf 37717 cytpfn 37786 ntrf 38421 uzmptshftfval 38545 binomcxplemrat 38549 addrfn 38676 subrfn 38677 mulvfn 38678 limsup10exlem 40004 liminfvalxr 40015 fourierdlem62 40385 fourierdlem70 40393 fourierdlem71 40394 fmtnorn 41446 zrinitorngc 42000 zrtermorngc 42001 zrtermoringc 42070 |
Copyright terms: Public domain | W3C validator |