![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > elmap | Structured version Unicode version |
Description: Membership relation for set exponentiation. (Contributed by NM, 8-Dec-2003.) |
Ref | Expression |
---|---|
elmap.1 |
![]() ![]() ![]() ![]() |
elmap.2 |
![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
elmap |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elmap.1 |
. 2
![]() ![]() ![]() ![]() | |
2 | elmap.2 |
. 2
![]() ![]() ![]() ![]() | |
3 | elmapg 7336 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 1, 2, 3 | mp2an 672 |
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 1592 ax-4 1603 ax-5 1671 ax-6 1710 ax-7 1730 ax-8 1760 ax-9 1762 ax-10 1777 ax-11 1782 ax-12 1794 ax-13 1955 ax-ext 2432 ax-sep 4520 ax-nul 4528 ax-pow 4577 ax-pr 4638 ax-un 6481 |
This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3an 967 df-tru 1373 df-ex 1588 df-nf 1591 df-sb 1703 df-eu 2266 df-mo 2267 df-clab 2440 df-cleq 2446 df-clel 2449 df-nfc 2604 df-ne 2649 df-ral 2803 df-rex 2804 df-rab 2807 df-v 3078 df-sbc 3293 df-dif 3438 df-un 3440 df-in 3442 df-ss 3449 df-nul 3745 df-if 3899 df-pw 3969 df-sn 3985 df-pr 3987 df-op 3991 df-uni 4199 df-br 4400 df-opab 4458 df-id 4743 df-xp 4953 df-rel 4954 df-cnv 4955 df-co 4956 df-dm 4957 df-rn 4958 df-iota 5488 df-fun 5527 df-fn 5528 df-f 5529 df-fv 5533 df-ov 6202 df-oprab 6203 df-mpt2 6204 df-map 7325 |
This theorem is referenced by: mapval2 7351 fvmptmap 7358 mapsn 7363 mapsnconst 7367 mapsncnv 7368 xpmapenlem 7587 pwfseqlem3 8937 tskcard 9058 ingru 9092 rpnnen1lem1 11089 rpnnen1lem3 11091 rpnnen1lem4 11092 rpnnen1lem5 11093 prmreclem2 14095 1arith 14105 vdwlem6 14164 vdwlem7 14165 vdwlem8 14166 vdwlem9 14167 vdwlem11 14169 vdwlem13 14171 isfunc 14892 isfuncd 14893 idfucl 14909 cofucl 14916 funcres2b 14925 wunfunc 14927 catcfuccl 15095 ismhm 15584 symgval 16002 dfrhm2 16930 isabv 17026 psrelbas 17572 psraddcl 17576 psrmulcllem 17580 psrvscacl 17586 psr0cl 17587 psrnegcl 17589 psr1cl 17595 subrgpsr 17614 mvrf 17620 mplmon 17665 mplcoe1 17667 coe1fval3 17787 00ply1bas 17817 ply1plusgfvi 17819 coe1z 17839 coe1mul2 17845 coe1tm 17849 pjdm 18256 pjfval2 18258 pnrmopn 19078 distgp 19801 indistgp 19802 elovolm 21089 elovolmr 21090 ovolmge0 21091 ovolgelb 21094 ovolunlem1a 21110 ovolunlem1 21111 ovoliunlem1 21116 ovoliunlem2 21117 ovolshftlem2 21124 ovolicc2 21136 ioombl1 21175 itg2seq 21352 coeeulem 21824 coeeq 21827 aannenlem1 21926 dvntaylp 21968 taylthlem1 21970 taylthlem2 21971 pserdvlem2 22025 sqff1o 22652 elee 23291 islno 24304 nmooval 24314 ajfval 24360 h2hcau 24532 h2hlm 24533 hcau 24737 hlimadd 24746 hhcms 24756 hlim0 24789 hhsscms 24831 pjmf1 25270 hosmval 25290 hommval 25291 hodmval 25292 hfsmval 25293 hfmmval 25294 elcnop 25412 ellnop 25413 elhmop 25428 hmopex 25430 nlfnval 25436 elcnfn 25437 ellnfn 25438 dmadjss 25442 dmadjop 25443 adjeu 25444 adjval 25445 hhcno 25459 hhcnf 25460 adjbdln 25638 isst 25768 ishst 25769 maprnin 26181 eulerpartleme 26889 eulerpartlemt 26897 eulerpartlemr 26900 eulerpartlemmf 26901 eulerpartlemgvv 26902 eulerpartlemgs2 26906 eulerpartlemn 26907 lgamgulmlem6 27163 isrngohom 28918 constmap 29196 mzpclall 29210 mzpf 29219 mzpindd 29229 mzpcompact2lem 29235 eldiophb 29242 mendrng 29696 dflinc2 31062 islfl 33028 islpolN 35451 |
Copyright terms: Public domain | W3C validator |