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 7750 | . 2 ⊢ (𝐴 ∈ V → dom 𝐴 ∈ V) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ dom 𝐴 ∈ V |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2106 Vcvv 3432 dom cdm 5589 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2709 ax-sep 5223 ax-nul 5230 ax-pr 5352 ax-un 7588 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1783 df-sb 2068 df-clab 2716 df-cleq 2730 df-clel 2816 df-rab 3073 df-v 3434 df-dif 3890 df-un 3892 df-in 3894 df-ss 3904 df-nul 4257 df-if 4460 df-sn 4562 df-pr 4564 df-op 4568 df-uni 4840 df-br 5075 df-opab 5137 df-cnv 5597 df-dm 5599 df-rn 5600 |
This theorem is referenced by: elxp4 7769 ofmres 7827 1stval 7833 fo1st 7851 frxp 7967 tfrlem8 8215 mapprc 8619 ixpprc 8707 bren 8743 brenOLD 8744 brdomg 8746 brdomgOLD 8747 fundmen 8821 domssex 8925 mapen 8928 ssenen 8938 hartogslem1 9301 wemapso 9310 brwdomn0 9328 unxpwdom2 9347 ixpiunwdom 9349 oemapwe 9452 cantnffval2 9453 r0weon 9768 fseqenlem2 9781 acndom 9807 acndom2 9810 dfac9 9892 ackbij2lem2 9996 ackbij2lem3 9997 cfsmolem 10026 coftr 10029 dcomex 10203 axdc3lem4 10209 axdclem 10275 axdclem2 10276 fodomb 10282 brdom3 10284 brdom5 10285 brdom4 10286 hashfacenOLD 14167 shftfval 14781 prdsvallem 17165 isoval 17477 issubc 17550 prfval 17916 psgnghm2 20786 dfac14 22769 indishmph 22949 ufldom 23113 tsmsval2 23281 dvmptadd 25124 dvmptmul 25125 dvmptco 25136 taylfval 25518 usgrsizedg 27582 usgredgleordALT 27601 vtxdun 27848 vtxdlfgrval 27852 vtxd0nedgb 27855 vtxdushgrfvedglem 27856 vtxdushgrfvedg 27857 vtxdginducedm1lem4 27909 vtxdginducedm1 27910 ewlksfval 27968 wksfval 27976 wksvOLD 27987 wlkiswwlksupgr2 28242 vdn0conngrumgrv2 28560 vdgn1frgrv2 28660 hmoval 29172 cyc3conja 31424 esum2d 32061 sitmval 32316 bnj893 32908 fmlafv 33342 fmla 33343 fmlasuc0 33346 frxp2 33791 frxp3 33797 dfrecs2 34252 dfrdg4 34253 indexdom 35892 dibfval 39155 aomclem1 40879 dfac21 40891 trclexi 41228 rtrclexi 41229 dfrtrcl5 41237 dfrcl2 41282 dvsubf 43455 dvdivf 43463 fouriersw 43772 smflimlem1 44306 smflimlem6 44311 smfpimcc 44341 smfsuplem1 44344 smfinflem 44350 smflimsuplem1 44353 smflimsuplem2 44354 smflimsuplem3 44355 smflimsuplem4 44356 smflimsuplem5 44357 smflimsuplem7 44359 smfliminflem 44363 upwlksfval 45297 |
Copyright terms: Public domain | W3C validator |