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 7097 | . 2 ⊢ (𝐴 ∈ V → dom 𝐴 ∈ V) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ dom 𝐴 ∈ V |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 1990 Vcvv 3200 dom cdm 5114 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-8 1992 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-sep 4781 ax-nul 4789 ax-pr 4906 ax-un 6949 |
This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3an 1039 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-rex 2918 df-rab 2921 df-v 3202 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-nul 3916 df-if 4087 df-sn 4178 df-pr 4180 df-op 4184 df-uni 4437 df-br 4654 df-opab 4713 df-cnv 5122 df-dm 5124 df-rn 5125 |
This theorem is referenced by: elxp4 7110 ofmres 7164 1stval 7170 fo1st 7188 frxp 7287 tfrlem8 7480 mapprc 7861 ixpprc 7929 bren 7964 brdomg 7965 ctex 7970 fundmen 8030 domssex 8121 mapen 8124 ssenen 8134 hartogslem1 8447 brwdomn0 8474 unxpwdom2 8493 ixpiunwdom 8496 oemapwe 8591 cantnffval2 8592 r0weon 8835 fseqenlem2 8848 acndom 8874 acndom2 8877 dfac9 8958 ackbij2lem2 9062 ackbij2lem3 9063 cfsmolem 9092 coftr 9095 dcomex 9269 axdc3lem4 9275 axdclem 9341 axdclem2 9342 fodomb 9348 brdom3 9350 brdom5 9351 brdom4 9352 hashfacen 13238 shftfval 13810 prdsval 16115 isoval 16425 issubc 16495 prfval 16839 symgbas 17800 psgnghm2 19927 dfac14 21421 indishmph 21601 ufldom 21766 tsmsval2 21933 dvmptadd 23723 dvmptmul 23724 dvmptco 23735 taylfval 24113 usgrsizedg 26107 usgredgleordALT 26126 vtxdun 26377 vtxdlfgrval 26381 vtxd0nedgb 26384 vtxdushgrfvedglem 26385 vtxdushgrfvedg 26386 vtxdginducedm1lem4 26438 vtxdginducedm1 26439 ewlksfval 26497 wksfval 26505 wksv 26515 wlkiswwlksupgr2 26763 vdn0conngrumgrv2 27056 vdgn1frgrv2 27160 hmoval 27665 esum2d 30155 sitmval 30411 bnj893 30998 dfrecs2 32057 dfrdg4 32058 indexdom 33529 dibfval 36430 aomclem1 37624 dfac21 37636 trclexi 37927 rtrclexi 37928 dfrtrcl5 37936 dfrcl2 37966 dvsubf 40128 dvdivf 40137 fouriersw 40448 smflimlem1 40979 smflimlem6 40984 smfpimcc 41014 smfsuplem1 41017 smfinflem 41023 smflimsuplem1 41026 smflimsuplem2 41027 smflimsuplem3 41028 smflimsuplem4 41029 smflimsuplem5 41030 smflimsuplem7 41032 smfliminflem 41036 upwlksfval 41716 |
Copyright terms: Public domain | W3C validator |