Theorem dmexg 7841

Description: The domain of a set is a set. Corollary 6.8(2) of [TakeutiZaring] p. 26. (Contributed by NM, 7-Apr-1995.)

Assertion

Ref	Expression
dmexg	⊢ (𝐴 ∈ 𝑉 → dom 𝐴 ∈ V)

Proof of Theorem dmexg

Step	Hyp	Ref	Expression
1		uniexg 7683	. 2 ⊢ (𝐴 ∈ 𝑉 → ∪ 𝐴 ∈ V)
2		uniexg 7683	. 2 ⊢ (∪ 𝐴 ∈ V → ∪ ∪ 𝐴 ∈ V)
3		ssun1 4107	. . . 4 ⊢ dom 𝐴 ⊆ (dom 𝐴 ∪ ran 𝐴)
4		dmrnssfld 5916	. . . 4 ⊢ (dom 𝐴 ∪ ran 𝐴) ⊆ ∪ ∪ 𝐴
5	3, 4	sstri 3924	. . 3 ⊢ dom 𝐴 ⊆ ∪ ∪ 𝐴
6		ssexg 5251	. . 3 ⊢ ((dom 𝐴 ⊆ ∪ ∪ 𝐴 ∧ ∪ ∪ 𝐴 ∈ V) → dom 𝐴 ∈ V)
7	5, 6	mpan 696	. 2 ⊢ (∪ ∪ 𝐴 ∈ V → dom 𝐴 ∈ V)
8	1, 2, 7	3syl 18	1 ⊢ (𝐴 ∈ 𝑉 → dom 𝐴 ∈ V)

Syntax hints:   → wi 4   ∈ wcel 2119  Vcvv 3431   ∪ cun 3881   ⊆ wss 3883  ∪ cuni 4838  dom cdm 5618  ran crn 5619

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711  ax-sep 5218  ax-pr 5362  ax-un 7678

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4262  df-if 4455  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-br 5073  df-opab 5135  df-cnv 5626  df-dm 5628  df-rn 5629

This theorem is referenced by:  dmexd  7843  dmfex  7845  dmex  7849  iprc  7851  exse2  7857  xpexr2  7859  xpexcnv  7860  soex  7861  cnvexg  7864  coexg  7869  cofunexg  7891  offval3  7924  opabn1stprc  8000  suppval  8102  funsssuppss  8130  suppssov1  8137  suppssov2  8138  suppssfv  8142  tposexg  8180  tfrlem12  8318  tfrlem13  8319  erexb  8659  f1vrnfibi  9242  oion  9441  ttrclexg  9635  fpwwe2lem3  10547  hashfn  14328  hashfundm  14395  hashf1dmrn  14396  fundmge2nop0  14455  fun2dmnop0  14457  trclexlem  14947  relexp0g  14975  relexpsucnnr  14978  o1of2  15566  isofn  17733  ssclem  17777  ssc2  17780  ssctr  17783  subsubc  17811  resf1st  17852  resf2nd  17853  funcres  17854  dprddomprc  19968  dprdval0prc  19970  subgdmdprd  20002  dprd2da  20010  decpmatval0  22747  pmatcollpw3lem  22766  ordtbaslem  23171  ordtuni  23173  ordtbas2  23174  ordtbas  23175  ordttopon  23176  ordtopn1  23177  ordtopn2  23178  txindislem  23616  ordthmeolem  23784  ptcmplem2  24036  tuslem  24249  dvnff  25908  bdayval  27630  noextend  27648  bdayfo  27659  vtxdgf  29558  fdifsuppconst  32781  ressupprn  32782  ofcfval3  34286  braew  34426  omsval  34477  sibfof  34524  sitmcl  34535  cndprobval  34617  tailf  36603  tailfb  36605  ismgmOLD  38217  dmqsex  38729  qmapex  38818  dfcnvrefrels2  38975  dfcnvrefrels3  38976  rclexi  44059  rtrclexlem  44060  cnvrcl0  44069  dfrtrcl5  44073  relexpmulg  44154  relexp01min  44157  relexpxpmin  44161  unidmex  45498  caragenval  46936  caragenunidm  46951  itcoval0  49153  itcoval1  49154  isofnALT  49521