![]() |
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 7357 | . 2 ⊢ (𝐴 ∈ V → dom 𝐴 ∈ V) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ dom 𝐴 ∈ V |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2166 Vcvv 3413 dom cdm 5341 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1896 ax-4 1910 ax-5 2011 ax-6 2077 ax-7 2114 ax-8 2168 ax-9 2175 ax-10 2194 ax-11 2209 ax-12 2222 ax-13 2390 ax-ext 2802 ax-sep 5004 ax-nul 5012 ax-pr 5126 ax-un 7208 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 881 df-3an 1115 df-tru 1662 df-ex 1881 df-nf 1885 df-sb 2070 df-mo 2604 df-eu 2639 df-clab 2811 df-cleq 2817 df-clel 2820 df-nfc 2957 df-rex 3122 df-rab 3125 df-v 3415 df-dif 3800 df-un 3802 df-in 3804 df-ss 3811 df-nul 4144 df-if 4306 df-sn 4397 df-pr 4399 df-op 4403 df-uni 4658 df-br 4873 df-opab 4935 df-cnv 5349 df-dm 5351 df-rn 5352 |
This theorem is referenced by: elxp4 7371 ofmres 7423 1stval 7429 fo1st 7447 frxp 7550 tfrlem8 7745 mapprc 8125 ixpprc 8195 bren 8230 brdomg 8231 ctex 8236 fundmen 8295 domssex 8389 mapen 8392 ssenen 8402 hartogslem1 8715 brwdomn0 8742 unxpwdom2 8761 ixpiunwdom 8764 oemapwe 8867 cantnffval2 8868 r0weon 9147 fseqenlem2 9160 acndom 9186 acndom2 9189 dfac9 9272 ackbij2lem2 9376 ackbij2lem3 9377 cfsmolem 9406 coftr 9409 dcomex 9583 axdc3lem4 9589 axdclem 9655 axdclem2 9656 fodomb 9662 brdom3 9664 brdom5 9665 brdom4 9666 hashfacen 13526 shftfval 14186 prdsval 16467 isoval 16776 issubc 16846 prfval 17191 symgbas 18149 psgnghm2 20285 dfac14 21791 indishmph 21971 ufldom 22135 tsmsval2 22302 dvmptadd 24121 dvmptmul 24122 dvmptco 24133 taylfval 24511 usgrsizedg 26510 usgredgleordALT 26530 vtxdun 26778 vtxdlfgrval 26782 vtxd0nedgb 26785 vtxdushgrfvedglem 26786 vtxdushgrfvedg 26787 vtxdginducedm1lem4 26839 vtxdginducedm1 26840 ewlksfval 26898 wksfval 26906 wksv 26916 wlkiswwlksupgr2 27175 vdn0conngrumgrv2 27571 vdgn1frgrv2 27676 hmoval 28219 esum2d 30699 sitmval 30955 bnj893 31543 dfrecs2 32595 dfrdg4 32596 cnfinltrel 33785 indexdom 34071 dibfval 37215 aomclem1 38466 dfac21 38478 trclexi 38767 rtrclexi 38768 dfrtrcl5 38776 dfrcl2 38806 dvsubf 40922 dvdivf 40931 fouriersw 41241 smflimlem1 41772 smflimlem6 41777 smfpimcc 41807 smfsuplem1 41810 smfinflem 41816 smflimsuplem1 41819 smflimsuplem2 41820 smflimsuplem3 41821 smflimsuplem4 41822 smflimsuplem5 41823 smflimsuplem7 41825 smfliminflem 41829 upwlksfval 42562 |
Copyright terms: Public domain | W3C validator |