![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > dmex | Structured version Visualization version GIF version |
Description: The domain of a set is a set. Corollary 6.8(2) of [TakeutiZaring] p. 26. (Contributed by NM, 7-Jul-2008.) |
Ref | Expression |
---|---|
dmex.1 | ⊢ 𝐴 ∈ V |
Ref | Expression |
---|---|
dmex | ⊢ dom 𝐴 ∈ V |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dmex.1 | . 2 ⊢ 𝐴 ∈ V | |
2 | dmexg 7903 | . 2 ⊢ (𝐴 ∈ V → dom 𝐴 ∈ V) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ dom 𝐴 ∈ V |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2099 Vcvv 3469 dom cdm 5672 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-ext 2698 ax-sep 5293 ax-nul 5300 ax-pr 5423 ax-un 7734 |
This theorem depends on definitions: df-bi 206 df-an 396 df-or 847 df-3an 1087 df-tru 1537 df-fal 1547 df-ex 1775 df-sb 2061 df-clab 2705 df-cleq 2719 df-clel 2805 df-rab 3428 df-v 3471 df-dif 3947 df-un 3949 df-in 3951 df-ss 3961 df-nul 4319 df-if 4525 df-sn 4625 df-pr 4627 df-op 4631 df-uni 4904 df-br 5143 df-opab 5205 df-cnv 5680 df-dm 5682 df-rn 5683 |
This theorem is referenced by: elxp4 7924 ofmres 7982 1stval 7989 fo1st 8007 frxp 8125 frxp2 8143 frxp3 8150 tfrlem8 8398 mapprc 8840 ixpprc 8929 bren 8965 brenOLD 8966 brdomg 8968 brdomgOLD 8969 fundmen 9047 domssex 9154 mapen 9157 ssenen 9167 hartogslem1 9557 wemapso 9566 brwdomn0 9584 unxpwdom2 9603 ixpiunwdom 9605 oemapwe 9709 cantnffval2 9710 r0weon 10027 fseqenlem2 10040 acndom 10066 acndom2 10069 dfac9 10151 ackbij2lem2 10255 ackbij2lem3 10256 cfsmolem 10285 coftr 10288 dcomex 10462 axdc3lem4 10468 axdclem 10534 axdclem2 10535 fodomb 10541 brdom3 10543 brdom5 10544 brdom4 10545 hashfacenOLD 14438 shftfval 15041 prdsvallem 17427 isoval 17739 issubc 17812 prfval 18181 psgnghm2 21500 psdmul 22077 dfac14 23509 indishmph 23689 ufldom 23853 tsmsval2 24021 dvmptadd 25879 dvmptmul 25880 dvmptco 25891 taylfval 26280 usgrsizedg 29015 usgredgleordALT 29034 vtxdun 29282 vtxdlfgrval 29286 vtxd0nedgb 29289 vtxdushgrfvedglem 29290 vtxdushgrfvedg 29291 vtxdginducedm1lem4 29343 vtxdginducedm1 29344 ewlksfval 29402 wksfval 29410 wksvOLD 29421 wlkiswwlksupgr2 29675 vdn0conngrumgrv2 29993 vdgn1frgrv2 30093 hmoval 30607 cyc3conja 32856 esum2d 33648 sitmval 33905 bnj893 34495 fmlafv 34926 fmla 34927 fmlasuc0 34930 dfrecs2 35482 dfrdg4 35483 indexdom 37142 dibfval 40551 aomclem1 42400 dfac21 42412 trclexi 42973 rtrclexi 42974 dfrtrcl5 42982 dfrcl2 43027 dvsubf 45225 dvdivf 45233 fouriersw 45542 smflimlem1 46082 smflimlem6 46087 smfpimcc 46119 smfsuplem1 46122 smfinflem 46128 smflimsuplem1 46131 smflimsuplem2 46132 smflimsuplem3 46133 smflimsuplem4 46134 smflimsuplem5 46135 smflimsuplem7 46137 smfliminflem 46141 fsupdm 46153 finfdm 46157 isuspgrim0 47093 grimidvtxedg 47097 upwlksfval 47120 |
Copyright terms: Public domain | W3C validator |