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 7646 | . 2 ⊢ (𝐴 ∈ V → dom 𝐴 ∈ V) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ dom 𝐴 ∈ V |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2114 Vcvv 3400 dom cdm 5535 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1975 ax-7 2020 ax-8 2116 ax-9 2124 ax-ext 2711 ax-sep 5177 ax-nul 5184 ax-pr 5306 ax-un 7491 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 847 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1787 df-sb 2075 df-clab 2718 df-cleq 2731 df-clel 2812 df-rab 3063 df-v 3402 df-dif 3856 df-un 3858 df-in 3860 df-ss 3870 df-nul 4222 df-if 4425 df-sn 4527 df-pr 4529 df-op 4533 df-uni 4807 df-br 5041 df-opab 5103 df-cnv 5543 df-dm 5545 df-rn 5546 |
This theorem is referenced by: elxp4 7665 ofmres 7722 1stval 7728 fo1st 7746 frxp 7858 tfrlem8 8061 mapprc 8453 ixpprc 8541 bren 8576 brdomg 8577 fundmen 8642 domssex 8740 mapen 8743 ssenen 8753 hartogslem1 9091 wemapso 9100 brwdomn0 9118 unxpwdom2 9137 ixpiunwdom 9139 oemapwe 9242 cantnffval2 9243 r0weon 9524 fseqenlem2 9537 acndom 9563 acndom2 9566 dfac9 9648 ackbij2lem2 9752 ackbij2lem3 9753 cfsmolem 9782 coftr 9785 dcomex 9959 axdc3lem4 9965 axdclem 10031 axdclem2 10032 fodomb 10038 brdom3 10040 brdom5 10041 brdom4 10042 hashfacenOLD 13917 shftfval 14531 prdsval 16843 isoval 17152 issubc 17222 prfval 17577 psgnghm2 20409 dfac14 22381 indishmph 22561 ufldom 22725 tsmsval2 22893 dvmptadd 24724 dvmptmul 24725 dvmptco 24736 taylfval 25118 usgrsizedg 27169 usgredgleordALT 27188 vtxdun 27435 vtxdlfgrval 27439 vtxd0nedgb 27442 vtxdushgrfvedglem 27443 vtxdushgrfvedg 27444 vtxdginducedm1lem4 27496 vtxdginducedm1 27497 ewlksfval 27555 wksfval 27563 wksv 27573 wlkiswwlksupgr2 27827 vdn0conngrumgrv2 28145 vdgn1frgrv2 28245 hmoval 28757 cyc3conja 31013 esum2d 31643 sitmval 31898 bnj893 32491 fmlafv 32925 fmla 32926 fmlasuc0 32929 frxp2 33416 frxp3 33422 dfrecs2 33907 dfrdg4 33908 indexdom 35547 dibfval 38810 aomclem1 40491 dfac21 40503 trclexi 40813 rtrclexi 40814 dfrtrcl5 40822 dfrcl2 40868 dvsubf 43037 dvdivf 43045 fouriersw 43354 smflimlem1 43885 smflimlem6 43890 smfpimcc 43920 smfsuplem1 43923 smfinflem 43929 smflimsuplem1 43932 smflimsuplem2 43933 smflimsuplem3 43934 smflimsuplem4 43935 smflimsuplem5 43936 smflimsuplem7 43938 smfliminflem 43942 upwlksfval 44878 |
Copyright terms: Public domain | W3C validator |