![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > mpt2ex | Structured version Visualization version Unicode version |
Description: If the domain of a function given by maps-to notation is a set, the function is a set. (Contributed by Mario Carneiro, 20-Dec-2013.) |
Ref | Expression |
---|---|
mpt2ex.1 |
![]() ![]() ![]() ![]() |
mpt2ex.2 |
![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
mpt2ex |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mpt2ex.1 |
. 2
![]() ![]() ![]() ![]() | |
2 | mpt2ex.2 |
. . 3
![]() ![]() ![]() ![]() | |
3 | 2 | rgenw 2761 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | eqid 2462 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | 4 | mpt2exxg 6899 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
6 | 1, 3, 5 | mp2an 683 |
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 1680 ax-4 1693 ax-5 1769 ax-6 1816 ax-7 1862 ax-8 1900 ax-9 1907 ax-10 1926 ax-11 1931 ax-12 1944 ax-13 2102 ax-ext 2442 ax-rep 4531 ax-sep 4541 ax-nul 4550 ax-pow 4598 ax-pr 4656 ax-un 6615 |
This theorem depends on definitions: df-bi 190 df-or 376 df-an 377 df-3an 993 df-tru 1458 df-ex 1675 df-nf 1679 df-sb 1809 df-eu 2314 df-mo 2315 df-clab 2449 df-cleq 2455 df-clel 2458 df-nfc 2592 df-ne 2635 df-ral 2754 df-rex 2755 df-reu 2756 df-rab 2758 df-v 3059 df-sbc 3280 df-csb 3376 df-dif 3419 df-un 3421 df-in 3423 df-ss 3430 df-nul 3744 df-if 3894 df-pw 3965 df-sn 3981 df-pr 3983 df-op 3987 df-uni 4213 df-iun 4294 df-br 4419 df-opab 4478 df-mpt 4479 df-id 4771 df-xp 4862 df-rel 4863 df-cnv 4864 df-co 4865 df-dm 4866 df-rn 4867 df-res 4868 df-ima 4869 df-iota 5569 df-fun 5607 df-fn 5608 df-f 5609 df-f1 5610 df-fo 5611 df-f1o 5612 df-fv 5613 df-oprab 6324 df-mpt2 6325 df-1st 6825 df-2nd 6826 |
This theorem is referenced by: qexALT 11313 ruclem13 14349 vdwapfval 14976 prdsco 15421 imasvsca 15476 homffval 15650 comfffval 15658 comffval 15659 comfffn 15664 comfeq 15666 oppccofval 15676 monfval 15692 sectffval 15710 invffval 15718 cofu1st 15843 cofu2nd 15845 cofucl 15848 natfval 15906 fuccofval 15919 fucco 15922 coafval 16014 setcco 16033 catchomfval 16048 catccofval 16050 catcco 16051 estrcco 16070 xpcval 16117 xpchomfval 16119 xpccofval 16122 xpcco 16123 1stf1 16132 1stf2 16133 2ndf1 16135 2ndf2 16136 1stfcl 16137 2ndfcl 16138 prf1 16140 prf2fval 16141 prfcl 16143 prf1st 16144 prf2nd 16145 evlf2 16158 evlf1 16160 evlfcl 16162 curf1fval 16164 curf11 16166 curf12 16167 curf1cl 16168 curf2 16169 curfcl 16172 hof1fval 16193 hof2fval 16195 hofcl 16199 yonedalem3 16220 mgmnsgrpex 16720 sgrpnmndex 16721 grpsubfval 16763 mulgfval 16814 symgplusg 17085 lsmfval 17345 pj1fval 17399 dvrfval 17967 psrmulr 18663 psrvscafval 18669 evlslem2 18790 mamufval 19465 mvmulfval 19622 isphtpy 22067 pcofval 22096 q1pval 23160 r1pval 23163 motplusg 24643 midf 24874 ismidb 24876 ttgval 24961 ebtwntg 25068 ecgrtg 25069 elntg 25070 vsfval 26310 dipfval 26394 smatfval 28672 lmatval 28690 qqhval 28829 dya2iocuni 29155 sxbrsigalem5 29160 sitmval 29232 signswplusg 29494 mclsrcl 30249 mclsval 30251 ldualfvs 32748 paddfval 33408 tgrpopr 34360 erngfplus 34415 erngfmul 34418 erngfplus-rN 34423 erngfmul-rN 34426 dvafvadd 34627 dvafvsca 34629 dvaabl 34638 dvhfvadd 34705 dvhfvsca 34714 djafvalN 34748 djhfval 35011 hlhilip 35565 mendplusgfval 36097 mendmulrfval 36099 mendvscafval 36102 hoidmvval 38506 cznrng 40326 cznnring 40327 rngchomfvalALTV 40355 rngccofvalALTV 40358 rngccoALTV 40359 ringchomfvalALTV 40418 ringccofvalALTV 40421 ringccoALTV 40422 |
Copyright terms: Public domain | W3C validator |