![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > fnmpti | Structured version Visualization version Unicode 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 |
![]() ![]() ![]() ![]() |
fnmpti.2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
fnmpti |
![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fnmpti.1 |
. . 3
![]() ![]() ![]() ![]() | |
2 | 1 | rgenw 2749 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | fnmpti.2 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 3 | mptfng 5703 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | 2, 4 | mpbi 212 |
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 1669 ax-4 1682 ax-5 1758 ax-6 1805 ax-7 1851 ax-9 1896 ax-10 1915 ax-11 1920 ax-12 1933 ax-13 2091 ax-ext 2431 ax-sep 4525 ax-nul 4534 ax-pr 4639 |
This theorem depends on definitions: df-bi 189 df-or 372 df-an 373 df-3an 987 df-tru 1447 df-ex 1664 df-nf 1668 df-sb 1798 df-eu 2303 df-mo 2304 df-clab 2438 df-cleq 2444 df-clel 2447 df-nfc 2581 df-ne 2624 df-ral 2742 df-rex 2743 df-rab 2746 df-v 3047 df-dif 3407 df-un 3409 df-in 3411 df-ss 3418 df-nul 3732 df-if 3882 df-sn 3969 df-pr 3971 df-op 3975 df-br 4403 df-opab 4462 df-mpt 4463 df-id 4749 df-xp 4840 df-rel 4841 df-cnv 4842 df-co 4843 df-dm 4844 df-fun 5584 df-fn 5585 |
This theorem is referenced by: dmmpti 5707 fconst 5769 dffn5 5910 eufnfv 6139 idref 6146 offn 6542 caofinvl 6558 fo1st 6813 fo2nd 6814 reldm 6844 mapsnf1o2 7519 unfilem2 7836 fidomdm 7853 pwfilem 7868 noinfep 8165 aceq3lem 8551 dfac4 8553 ackbij2lem2 8670 cfslb2n 8698 axcc2lem 8866 konigthlem 8993 rankcf 9202 tskuni 9208 seqf1o 12254 ccatlen 12721 ccatvalfn 12726 swrdlen 12779 swrdswrd 12816 sqrtf 13426 mptfzshft 13839 fsumrev 13840 fprodrev 14031 efcvgfsum 14140 prmreclem2 14861 1arith 14871 vdwlem6 14936 vdwlem8 14938 slotfn 15135 topnfn 15324 fnmre 15497 cidffn 15584 cidfn 15585 funcres 15801 yonedainv 16166 fn0g 16505 grpinvfn 16706 conjnmz 16916 psgnfn 17142 odf 17186 odfOLD 17202 sylow1lem4 17253 pgpssslw 17266 sylow2blem3 17274 sylow3lem2 17280 cygctb 17526 dprd2da 17675 fnmgp 17725 rlmfn 18413 rrgsupp 18515 asclfn 18560 evlslem1 18738 frlmup4 19359 mdetrlin 19627 fncld 20037 hauseqlcld 20661 kqf 20762 filunirn 20897 fmf 20960 txflf 21021 clsnsg 21124 tgpconcomp 21127 qustgpopn 21134 qustgplem 21135 ustfn 21216 xmetunirn 21352 met1stc 21536 rrxmvallem 22358 ovolf 22435 vitali 22571 i1fmulc 22661 mbfi1fseqlem4 22676 itg2seq 22700 itg2monolem1 22708 i1fibl 22765 fncpn 22887 lhop1lem 22965 mdegxrf 23017 aannenlem3 23286 efabl 23499 logccv 23608 padicabvf 24469 mptelee 24925 wlkiswwlk2lem1 25419 clwlkisclwwlklem2a2 25508 fngid 25942 grpoinvf 25968 occllem 26956 pjfni 27354 pjmfn 27368 rnbra 27760 bra11 27761 kbass2 27770 hmopidmchi 27804 xppreima2 28249 abfmpunirn 28251 dmct 28298 psgnfzto1stlem 28613 fimaproj 28660 locfinreflem 28667 ofcfn 28921 sxbrsigalem3 29094 eulerpartgbij 29205 sseqfv1 29222 sseqfn 29223 sseqf 29225 sseqfv2 29227 signstlen 29456 msubrn 30167 msrf 30180 faclimlem1 30379 poimirlem30 31970 mblfinlem2 31978 volsupnfl 31985 cnambfre 31989 itg2addnclem2 31994 itg2addnclem3 31995 ftc1anclem5 32021 ftc1anclem7 32023 sdclem2 32071 prdsbnd2 32127 rrncmslem 32164 diafn 34602 cdlemm10N 34686 dibfna 34722 lcfrlem9 35118 mapd1o 35216 hdmapfnN 35400 hgmapfnN 35459 rmxypairf1o 35759 hbtlem6 35988 dgraaf 36011 dgraafOLD 36012 cytpfn 36085 uzmptshftfval 36695 binomcxplemrat 36699 addrfn 36825 subrfn 36826 mulvfn 36827 fourierdlem62 38032 fourierdlem70 38040 fourierdlem71 38041 zrinitorngc 40055 zrtermorngc 40056 zrtermoringc 40125 |
Copyright terms: Public domain | W3C validator |