Theorem dmexg 7826

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 7668	. 2 ⊢ (𝐴 ∈ 𝑉 → ∪ 𝐴 ∈ V)
2		uniexg 7668	. 2 ⊢ (∪ 𝐴 ∈ V → ∪ ∪ 𝐴 ∈ V)
3		ssun1 4123	. . . 4 ⊢ dom 𝐴 ⊆ (dom 𝐴 ∪ ran 𝐴)
4		dmrnssfld 5908	. . . 4 ⊢ (dom 𝐴 ∪ ran 𝐴) ⊆ ∪ ∪ 𝐴
5	3, 4	sstri 3939	. . 3 ⊢ dom 𝐴 ⊆ ∪ ∪ 𝐴
6		ssexg 5256	. . 3 ⊢ ((dom 𝐴 ⊆ ∪ ∪ 𝐴 ∧ ∪ ∪ 𝐴 ∈ V) → dom 𝐴 ∈ V)
7	5, 6	mpan 690	. 2 ⊢ (∪ ∪ 𝐴 ∈ V → dom 𝐴 ∈ V)
8	1, 2, 7	3syl 18	1 ⊢ (𝐴 ∈ 𝑉 → dom 𝐴 ∈ V)

Syntax hints:   → wi 4   ∈ wcel 2111  Vcvv 3436   ∪ cun 3895   ⊆ wss 3897  ∪ cuni 4854  dom cdm 5611  ran crn 5612

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703  ax-sep 5229  ax-nul 5239  ax-pr 5365  ax-un 7663

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-nul 4279  df-if 4471  df-sn 4572  df-pr 4574  df-op 4578  df-uni 4855  df-br 5087  df-opab 5149  df-cnv 5619  df-dm 5621  df-rn 5622

This theorem is referenced by:  dmexd  7828  dmfex  7830  dmex  7834  iprc  7836  exse2  7842  xpexr2  7844  xpexcnv  7845  soex  7846  cnvexg  7849  coexg  7854  cofunexg  7876  offval3  7909  opabn1stprc  7985  suppval  8087  funsssuppss  8115  suppssov1  8122  suppssov2  8123  suppssfv  8127  tposexg  8165  tfrlem12  8303  tfrlem13  8304  erexb  8642  f1vrnfibi  9221  oion  9417  ttrclexg  9608  fpwwe2lem3  10519  hashfn  14277  hashfundm  14344  hashf1dmrn  14345  fundmge2nop0  14404  fun2dmnop0  14406  trclexlem  14896  relexp0g  14924  relexpsucnnr  14927  o1of2  15515  isofn  17677  ssclem  17721  ssc2  17724  ssctr  17727  subsubc  17755  resf1st  17796  resf2nd  17797  funcres  17798  dprddomprc  19909  dprdval0prc  19911  subgdmdprd  19943  dprd2da  19951  decpmatval0  22674  pmatcollpw3lem  22693  ordtbaslem  23098  ordtuni  23100  ordtbas2  23101  ordtbas  23102  ordttopon  23103  ordtopn1  23104  ordtopn2  23105  txindislem  23543  ordthmeolem  23711  ptcmplem2  23963  tuslem  24176  dvnff  25847  bdayval  27582  noextend  27600  bdayfo  27611  vtxdgf  29445  fdifsuppconst  32662  ressupprn  32663  ofcfval3  34107  braew  34247  omsval  34298  sibfof  34345  sitmcl  34356  cndprobval  34438  tailf  36409  tailfb  36411  ismgmOLD  37890  dfcnvrefrels2  38565  dfcnvrefrels3  38566  rclexi  43648  rtrclexlem  43649  cnvrcl0  43658  dfrtrcl5  43662  relexpmulg  43743  relexp01min  43746  relexpxpmin  43750  unidmex  45087  caragenval  46531  caragenunidm  46546  itcoval0  48694  itcoval1  48695  isofnALT  49063