![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > fex | Structured version Visualization version Unicode version |
Description: If the domain of a mapping is a set, the function is a set. (Contributed by NM, 3-Oct-1999.) |
Ref | Expression |
---|---|
fex |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ffn 5750 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | fnex 6156 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | sylan 478 |
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 1679 ax-4 1692 ax-5 1768 ax-6 1815 ax-7 1861 ax-9 1906 ax-10 1925 ax-11 1930 ax-12 1943 ax-13 2101 ax-ext 2441 ax-rep 4528 ax-sep 4538 ax-nul 4547 ax-pr 4652 |
This theorem depends on definitions: df-bi 190 df-or 376 df-an 377 df-3an 993 df-tru 1457 df-ex 1674 df-nf 1678 df-sb 1808 df-eu 2313 df-mo 2314 df-clab 2448 df-cleq 2454 df-clel 2457 df-nfc 2591 df-ne 2634 df-ral 2753 df-rex 2754 df-reu 2755 df-rab 2757 df-v 3058 df-sbc 3279 df-csb 3375 df-dif 3418 df-un 3420 df-in 3422 df-ss 3429 df-nul 3743 df-if 3893 df-sn 3980 df-pr 3982 df-op 3986 df-uni 4212 df-iun 4293 df-br 4416 df-opab 4475 df-mpt 4476 df-id 4767 df-xp 4858 df-rel 4859 df-cnv 4860 df-co 4861 df-dm 4862 df-rn 4863 df-res 4864 df-ima 4865 df-iota 5564 df-fun 5602 df-fn 5603 df-f 5604 df-f1 5605 df-fo 5606 df-f1o 5607 df-fv 5608 |
This theorem is referenced by: f1oexrnex 6768 frnsuppeq 6952 suppsnop 6954 f1domg 7614 fdmfisuppfi 7917 frnfsuppbi 7937 fsuppco2 7941 fsuppcor 7942 mapfienlem2 7944 ordtypelem10 8067 oiexg 8075 cnfcom3clem 8235 infxpenc2lem2 8476 fin23lem32 8799 isf32lem10 8817 hashf1rn 12566 hashf1lem1 12650 fz1isolem 12656 iswrd 12704 climsup 13781 fsum 13834 supcvg 13962 fprod 14043 vdwmc 14976 vdwpc 14978 ramval 15008 ramvalOLD 15009 imasval 15459 imasvalOLD 15460 imasle 15472 pwsco1mhm 16665 isghm 16931 elsymgbas 17071 gsumval3a 17585 gsumval3lem1 17587 gsumval3lem2 17588 gsumzres 17591 gsumzf1o 17594 gsumzaddlem 17602 gsumzadd 17603 gsumzmhm 17618 gsumzoppg 17625 gsumpt 17642 gsum2dlem2 17651 dmdprd 17678 prdslmodd 18240 gsumply1subr 18875 dsmmsubg 19354 dsmmlss 19355 islindf2 19420 f1lindf 19428 islindf4 19444 prdstps 20692 qtopval2 20759 tsmsres 21206 climcncf 21980 itg2gt0 22766 ulmval 23383 pserulm 23425 jensen 23962 isismt 24627 iseupa 25741 isgrpoi 25974 isgrp2d 26011 isgrpda 26073 elghomlem2OLD 26138 isrngod 26155 vcoprne 26246 isvc 26248 isnv 26279 cnnvg 26357 cnnvs 26360 cnnvnm 26361 cncph 26508 ajval 26551 hvmulex 26712 hhph 26879 hlimi 26889 chlimi 26935 hhssva 26958 hhsssm 26959 hhssnm 26960 hhshsslem1 26966 elunop 27573 adjeq 27636 leoprf2 27828 fpwrelmapffslem 28365 lmdvg 28807 esumpfinvallem 28943 ofcfval4 28974 omsfval 29166 omsf 29168 omsfvalOLD 29170 omsfOLD 29172 omssubadd 29176 omssubaddOLD 29180 carsgval 29183 eulerpartgbij 29253 eulerpartlemmf 29256 sseqval 29269 subfacp1lem5 29955 sinccvglem 30364 elno 30581 filnetlem4 31085 bj-finsumval0 31746 poimirlem24 32008 mbfresfi 32031 iscringd 32276 islaut 33692 ispautN 33708 istendo 34371 binomcxplemnotnn0 36748 fidmfisupp 37516 climexp 37720 climinf 37721 climinfOLD 37722 limsupre 37758 limsupreOLD 37759 stirlinglem8 37980 fourierdlem70 38077 fourierdlem71 38078 fourierdlem80 38087 sge0val 38245 sge0f1o 38261 ismea 38326 meadjiunlem 38340 isomennd 38389 usgra2pth 39940 isassintop 40118 fdivmpt 40623 elbigolo1 40640 |
Copyright terms: Public domain | W3C validator |