![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ovmpt2a | Structured version Visualization version Unicode version |
Description: Value of an operation given by a maps-to rule. (Contributed by NM, 19-Dec-2013.) |
Ref | Expression |
---|---|
ovmpt2ga.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
ovmpt2ga.2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
ovmpt2a.4 |
![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
ovmpt2a |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ovmpt2a.4 |
. 2
![]() ![]() ![]() ![]() | |
2 | ovmpt2ga.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | ovmpt2ga.2 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 2, 3 | ovmpt2ga 6426 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | 1, 4 | mp3an3 1353 |
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-sbc 3268 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-uni 4199 df-br 4403 df-opab 4462 df-id 4749 df-xp 4840 df-rel 4841 df-cnv 4842 df-co 4843 df-dm 4844 df-iota 5546 df-fun 5584 df-fv 5590 df-ov 6293 df-oprab 6294 df-mpt2 6295 |
This theorem is referenced by: 1st2val 6819 2nd2val 6820 cantnffval 8168 cantnfsuc 8175 fseqenlem1 8455 xaddval 11516 xmulval 11518 fzoval 11921 expval 12274 ccatfval 12719 splcl 12859 cshfn 12892 bpolylem 14101 ruclem1 14283 sadfval 14426 sadcp1 14429 smufval 14451 smupp1 14454 eucalgval2 14540 pcval 14794 pc0 14804 vdwapval 14923 pwsval 15384 xpsfval 15473 xpsval 15478 rescval 15732 isfunc 15769 isfull 15815 isfth 15819 natfval 15851 catcisolem 16001 xpchom 16065 1stfval 16076 2ndfval 16079 yonedalem3a 16159 yonedainv 16166 plusfval 16494 ismhm 16584 mulgval 16760 eqgfval 16865 isga 16945 subgga 16954 cayleylem1 17053 sylow1lem2 17251 isslw 17260 sylow2blem1 17272 sylow3lem1 17279 sylow3lem6 17284 frgpuptinv 17421 frgpup2 17426 isrhm 17949 scafval 18110 islmhm 18250 psrmulfval 18609 mplval 18652 ltbval 18695 mpfrcl 18741 evlsval 18742 evlval 18747 xrsdsval 19012 ipfval 19216 dsmmval 19297 matval 19436 submafval 19604 mdetfval 19611 minmar1fval 19671 txval 20579 xkoval 20602 hmeofval 20773 flffval 21004 qustgplem 21135 dscmet 21587 dscopn 21588 tngval 21647 nmofval 21719 nghmfval 21727 nmofvalOLD 21738 nghmfvalOLD 21745 isnmhm 21767 htpyco1 22009 htpycc 22011 phtpycc 22022 reparphti 22028 pcoval 22042 pcohtpylem 22050 pcorevlem 22057 dyadval 22550 itg1addlem3 22656 itg1addlem4 22657 mbfi1fseqlem3 22675 mbfi1fseqlem4 22676 mbfi1fseqlem5 22677 mbfi1fseqlem6 22678 mdegfval 23011 quotval 23245 elqaalem2 23273 elqaalem2OLD 23276 cxpval 23609 cxpcn3 23688 angval 23730 sgmval 24069 lgsval 24228 clwwlknprop 25500 rusgranumwlklem2 25678 numclwwlkovf 25809 numclwwlkovg 25815 numclwwlkovq 25827 numclwwlkovh 25829 shsval 26965 sshjval 27003 faeval 29069 txsconlem 29963 cvxscon 29966 iscvm 29982 cvmliftlem5 30012 rngohomval 32203 rngoisoval 32216 rmxfval 35752 rmyfval 35753 mendplusg 36052 mendvsca 36057 addrval 36819 subrval 36820 mulvval 36821 sigarval 38459 ismgmhm 39836 dmatALTval 40246 |
Copyright terms: Public domain | W3C validator |