![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > dmexg | 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-Apr-1995.) |
Ref | Expression |
---|---|
dmexg | ⊢ (𝐴 ∈ 𝑉 → dom 𝐴 ∈ V) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | uniexg 7758 | . 2 ⊢ (𝐴 ∈ 𝑉 → ∪ 𝐴 ∈ V) | |
2 | uniexg 7758 | . 2 ⊢ (∪ 𝐴 ∈ V → ∪ ∪ 𝐴 ∈ V) | |
3 | ssun1 4187 | . . . 4 ⊢ dom 𝐴 ⊆ (dom 𝐴 ∪ ran 𝐴) | |
4 | dmrnssfld 5986 | . . . 4 ⊢ (dom 𝐴 ∪ ran 𝐴) ⊆ ∪ ∪ 𝐴 | |
5 | 3, 4 | sstri 4004 | . . 3 ⊢ dom 𝐴 ⊆ ∪ ∪ 𝐴 |
6 | ssexg 5328 | . . 3 ⊢ ((dom 𝐴 ⊆ ∪ ∪ 𝐴 ∧ ∪ ∪ 𝐴 ∈ V) → dom 𝐴 ∈ V) | |
7 | 5, 6 | mpan 690 | . 2 ⊢ (∪ ∪ 𝐴 ∈ V → dom 𝐴 ∈ V) |
8 | 1, 2, 7 | 3syl 18 | 1 ⊢ (𝐴 ∈ 𝑉 → dom 𝐴 ∈ V) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2105 Vcvv 3477 ∪ cun 3960 ⊆ wss 3962 ∪ cuni 4911 dom cdm 5688 ran crn 5689 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1791 ax-4 1805 ax-5 1907 ax-6 1964 ax-7 2004 ax-8 2107 ax-9 2115 ax-ext 2705 ax-sep 5301 ax-nul 5311 ax-pr 5437 ax-un 7753 |
This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1539 df-fal 1549 df-ex 1776 df-sb 2062 df-clab 2712 df-cleq 2726 df-clel 2813 df-rab 3433 df-v 3479 df-dif 3965 df-un 3967 df-in 3969 df-ss 3979 df-nul 4339 df-if 4531 df-sn 4631 df-pr 4633 df-op 4637 df-uni 4912 df-br 5148 df-opab 5210 df-cnv 5696 df-dm 5698 df-rn 5699 |
This theorem is referenced by: dmexd 7925 dmfex 7927 dmex 7931 iprc 7933 exse2 7939 xpexr2 7941 xpexcnv 7942 soex 7943 cnvexg 7946 coexg 7951 cofunexg 7971 offval3 8005 opabn1stprc 8081 suppval 8185 funsssuppss 8213 suppssov1 8220 suppssov2 8221 suppssfv 8225 tposexg 8263 tfrlem12 8427 tfrlem13 8428 erexb 8768 f1vrnfibi 9379 oion 9573 ttrclexg 9760 fpwwe2lem3 10670 hashfn 14410 hashfundm 14477 hashf1dmrn 14478 fundmge2nop0 14537 fun2dmnop0 14539 trclexlem 15029 relexp0g 15057 relexpsucnnr 15060 o1of2 15645 isofn 17822 ssclem 17866 ssc2 17869 ssctr 17872 subsubc 17903 resf1st 17944 resf2nd 17945 funcres 17946 dprddomprc 20034 dprdval0prc 20036 subgdmdprd 20068 dprd2da 20076 decpmatval0 22785 pmatcollpw3lem 22804 ordtbaslem 23211 ordtuni 23213 ordtbas2 23214 ordtbas 23215 ordttopon 23216 ordtopn1 23217 ordtopn2 23218 txindislem 23656 ordthmeolem 23824 ptcmplem2 24076 tuslem 24290 tuslemOLD 24291 dvnff 25973 bdayval 27707 noextend 27725 bdayfo 27736 vtxdgf 29503 fdifsuppconst 32703 ressupprn 32704 ofcfval3 34082 braew 34222 omsval 34274 sibfof 34321 sitmcl 34332 cndprobval 34414 tailf 36357 tailfb 36359 ismgmOLD 37836 dfcnvrefrels2 38509 dfcnvrefrels3 38510 rclexi 43604 rtrclexlem 43605 cnvrcl0 43614 dfrtrcl5 43618 relexpmulg 43699 relexp01min 43702 relexpxpmin 43706 unidmex 44989 caragenval 46448 caragenunidm 46463 itcoval0 48511 itcoval1 48512 |
Copyright terms: Public domain | W3C validator |