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 7456 | . 2 ⊢ (𝐴 ∈ 𝑉 → ∪ 𝐴 ∈ V) | |
2 | uniexg 7456 | . 2 ⊢ (∪ 𝐴 ∈ V → ∪ ∪ 𝐴 ∈ V) | |
3 | ssun1 4145 | . . . 4 ⊢ dom 𝐴 ⊆ (dom 𝐴 ∪ ran 𝐴) | |
4 | dmrnssfld 5834 | . . . 4 ⊢ (dom 𝐴 ∪ ran 𝐴) ⊆ ∪ ∪ 𝐴 | |
5 | 3, 4 | sstri 3973 | . . 3 ⊢ dom 𝐴 ⊆ ∪ ∪ 𝐴 |
6 | ssexg 5218 | . . 3 ⊢ ((dom 𝐴 ⊆ ∪ ∪ 𝐴 ∧ ∪ ∪ 𝐴 ∈ V) → dom 𝐴 ∈ V) | |
7 | 5, 6 | mpan 686 | . 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 3492 ∪ cun 3931 ⊆ wss 3933 ∪ cuni 4830 dom cdm 5548 ran crn 5549 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2151 ax-12 2167 ax-ext 2790 ax-sep 5194 ax-nul 5201 ax-pr 5320 ax-un 7450 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-3an 1081 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 df-mo 2615 df-eu 2647 df-clab 2797 df-cleq 2811 df-clel 2890 df-nfc 2960 df-rex 3141 df-rab 3144 df-v 3494 df-dif 3936 df-un 3938 df-in 3940 df-ss 3949 df-nul 4289 df-if 4464 df-sn 4558 df-pr 4560 df-op 4564 df-uni 4831 df-br 5058 df-opab 5120 df-cnv 5556 df-dm 5558 df-rn 5559 |
This theorem is referenced by: dmexd 7604 dmex 7605 iprc 7607 exse2 7611 xpexr2 7613 xpexcnv 7614 soex 7615 cnvexg 7618 coexg 7623 dmfex 7630 cofunexg 7639 offval3 7672 opabn1stprc 7745 suppval 7821 funsssuppss 7845 suppss 7849 suppssov1 7851 suppssfv 7855 tposexg 7895 tfrlem12 8014 tfrlem13 8015 erexb 8303 f1vrnfibi 8797 oion 8988 fpwwe2lem3 10043 hashfn 13724 fundmge2nop0 13838 fun2dmnop0 13840 trclexlem 14342 relexp0g 14369 relexpsucnnr 14372 o1of2 14957 isofn 17033 ssclem 17077 ssc2 17080 ssctr 17083 subsubc 17111 resf1st 17152 resf2nd 17153 funcres 17154 dprddomprc 19051 dprdval0prc 19053 subgdmdprd 19085 dprd2da 19093 decpmatval0 21300 pmatcollpw3lem 21319 ordtbaslem 21724 ordtuni 21726 ordtbas2 21727 ordtbas 21728 ordttopon 21729 ordtopn1 21730 ordtopn2 21731 txindislem 22169 ordthmeolem 22337 ptcmplem2 22589 tuslem 22803 dvnff 24447 vtxdgf 27180 ofcfval3 31260 braew 31400 omsval 31450 sibfof 31497 sitmcl 31508 cndprobval 31590 hashfundm 32251 hashf1dmrn 32252 bdayval 33052 noextend 33070 bdayfo 33079 tailf 33620 tailfb 33622 ismgmOLD 35009 dfcnvrefrels2 35646 dfcnvrefrels3 35647 rclexi 39853 rtrclexlem 39854 cnvrcl0 39863 dfrtrcl5 39867 relexpmulg 39933 relexp01min 39936 relexpxpmin 39940 unidmex 41189 caragenval 42652 caragenunidm 42667 |
Copyright terms: Public domain | W3C validator |