![]() |
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 7749 | . 2 ⊢ (𝐴 ∈ 𝑉 → ∪ 𝐴 ∈ V) | |
2 | uniexg 7749 | . 2 ⊢ (∪ 𝐴 ∈ V → ∪ ∪ 𝐴 ∈ V) | |
3 | ssun1 4172 | . . . 4 ⊢ dom 𝐴 ⊆ (dom 𝐴 ∪ ran 𝐴) | |
4 | dmrnssfld 5975 | . . . 4 ⊢ (dom 𝐴 ∪ ran 𝐴) ⊆ ∪ ∪ 𝐴 | |
5 | 3, 4 | sstri 3989 | . . 3 ⊢ dom 𝐴 ⊆ ∪ ∪ 𝐴 |
6 | ssexg 5325 | . . 3 ⊢ ((dom 𝐴 ⊆ ∪ ∪ 𝐴 ∧ ∪ ∪ 𝐴 ∈ V) → dom 𝐴 ∈ V) | |
7 | 5, 6 | mpan 688 | . 2 ⊢ (∪ ∪ 𝐴 ∈ V → dom 𝐴 ∈ V) |
8 | 1, 2, 7 | 3syl 18 | 1 ⊢ (𝐴 ∈ 𝑉 → dom 𝐴 ∈ V) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2098 Vcvv 3471 ∪ cun 3945 ⊆ wss 3947 ∪ cuni 4910 dom cdm 5680 ran crn 5681 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-ext 2698 ax-sep 5301 ax-nul 5308 ax-pr 5431 ax-un 7744 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-sb 2060 df-clab 2705 df-cleq 2719 df-clel 2805 df-rab 3429 df-v 3473 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-nul 4325 df-if 4531 df-sn 4631 df-pr 4633 df-op 4637 df-uni 4911 df-br 5151 df-opab 5213 df-cnv 5688 df-dm 5690 df-rn 5691 |
This theorem is referenced by: dmexd 7915 dmfex 7917 dmex 7921 iprc 7923 exse2 7929 xpexr2 7931 xpexcnv 7932 soex 7933 cnvexg 7936 coexg 7941 cofunexg 7956 offval3 7990 opabn1stprc 8066 suppval 8171 funsssuppss 8199 suppssOLD 8204 suppssov1 8207 suppssov2 8208 suppssfv 8212 tposexg 8250 tfrlem12 8414 tfrlem13 8415 erexb 8754 f1vrnfibi 9367 oion 9565 ttrclexg 9752 fpwwe2lem3 10662 hashfn 14372 hashfundm 14439 hashf1dmrn 14440 fundmge2nop0 14491 fun2dmnop0 14493 trclexlem 14979 relexp0g 15007 relexpsucnnr 15010 o1of2 15595 isofn 17763 ssclem 17807 ssc2 17810 ssctr 17813 subsubc 17844 resf1st 17885 resf2nd 17886 funcres 17887 dprddomprc 19962 dprdval0prc 19964 subgdmdprd 19996 dprd2da 20004 decpmatval0 22684 pmatcollpw3lem 22703 ordtbaslem 23110 ordtuni 23112 ordtbas2 23113 ordtbas 23114 ordttopon 23115 ordtopn1 23116 ordtopn2 23117 txindislem 23555 ordthmeolem 23723 ptcmplem2 23975 tuslem 24189 tuslemOLD 24190 dvnff 25871 bdayval 27599 noextend 27617 bdayfo 27628 vtxdgf 29303 fdifsuppconst 32487 ressupprn 32488 ofcfval3 33726 braew 33866 omsval 33918 sibfof 33965 sitmcl 33976 cndprobval 34058 tailf 35864 tailfb 35866 ismgmOLD 37328 dfcnvrefrels2 38004 dfcnvrefrels3 38005 rclexi 43048 rtrclexlem 43049 cnvrcl0 43058 dfrtrcl5 43062 relexpmulg 43143 relexp01min 43146 relexpxpmin 43150 unidmex 44417 caragenval 45883 caragenunidm 45898 itcoval0 47786 itcoval1 47787 |
Copyright terms: Public domain | W3C validator |