![]() |
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 7215 | . 2 ⊢ (𝐴 ∈ 𝑉 → ∪ 𝐴 ∈ V) | |
2 | uniexg 7215 | . 2 ⊢ (∪ 𝐴 ∈ V → ∪ ∪ 𝐴 ∈ V) | |
3 | ssun1 4003 | . . . 4 ⊢ dom 𝐴 ⊆ (dom 𝐴 ∪ ran 𝐴) | |
4 | dmrnssfld 5617 | . . . 4 ⊢ (dom 𝐴 ∪ ran 𝐴) ⊆ ∪ ∪ 𝐴 | |
5 | 3, 4 | sstri 3836 | . . 3 ⊢ dom 𝐴 ⊆ ∪ ∪ 𝐴 |
6 | ssexg 5029 | . . 3 ⊢ ((dom 𝐴 ⊆ ∪ ∪ 𝐴 ∧ ∪ ∪ 𝐴 ∈ V) → dom 𝐴 ∈ V) | |
7 | 5, 6 | mpan 683 | . 2 ⊢ (∪ ∪ 𝐴 ∈ V → dom 𝐴 ∈ V) |
8 | 1, 2, 7 | 3syl 18 | 1 ⊢ (𝐴 ∈ 𝑉 → dom 𝐴 ∈ V) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2166 Vcvv 3414 ∪ cun 3796 ⊆ wss 3798 ∪ cuni 4658 dom cdm 5342 ran crn 5343 |
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 2391 ax-ext 2803 ax-sep 5005 ax-nul 5013 ax-pr 5127 ax-un 7209 |
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 2605 df-eu 2640 df-clab 2812 df-cleq 2818 df-clel 2821 df-nfc 2958 df-rex 3123 df-rab 3126 df-v 3416 df-dif 3801 df-un 3803 df-in 3805 df-ss 3812 df-nul 4145 df-if 4307 df-sn 4398 df-pr 4400 df-op 4404 df-uni 4659 df-br 4874 df-opab 4936 df-cnv 5350 df-dm 5352 df-rn 5353 |
This theorem is referenced by: dmexd 7360 dmex 7361 iprc 7363 exse2 7367 xpexr2 7369 xpexcnv 7370 soex 7371 cnvexg 7374 coexg 7379 dmfex 7386 cofunexg 7392 offval3 7422 opabn1stprc 7490 suppval 7561 funsssuppss 7586 suppss 7590 suppssov1 7592 suppssfv 7596 tposexg 7631 tfrlem12 7751 tfrlem13 7752 erexb 8034 f1vrnfibi 8520 oion 8710 fpwwe2lem3 9770 hashfn 13454 fundmge2nop0 13563 fun2dmnop0 13565 trclexlem 14112 relexp0g 14139 relexpsucnnr 14142 o1of2 14720 isofn 16787 ssclem 16831 ssc2 16834 ssctr 16837 subsubc 16865 resf1st 16906 resf2nd 16907 funcres 16908 dprddomprc 18753 dprdval0prc 18755 subgdmdprd 18787 dprd2da 18795 decpmatval0 20939 pmatcollpw3lem 20958 ordtbaslem 21363 ordtuni 21365 ordtbas2 21366 ordtbas 21367 ordttopon 21368 ordtopn1 21369 ordtopn2 21370 txindislem 21807 ordthmeolem 21975 ptcmplem2 22227 tuslem 22441 dvnff 24085 vtxdgf 26769 ofcfval3 30709 braew 30850 omsval 30900 sibfof 30947 sitmcl 30958 cndprobval 31041 bdayval 32340 noextend 32358 bdayfo 32367 tailf 32908 tailfb 32910 ismgmOLD 34191 dfcnvrefrels2 34824 dfcnvrefrels3 34825 rclexi 38763 rtrclexlem 38764 cnvrcl0 38773 dfrtrcl5 38777 relexpmulg 38843 relexp01min 38846 relexpxpmin 38850 unidmex 40034 caragenval 41501 caragenunidm 41516 offval0 43146 |
Copyright terms: Public domain | W3C validator |