Theorem dmexg 7894

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 7730	. 2 ⊢ (𝐴 ∈ 𝑉 → ∪ 𝐴 ∈ V)
2		uniexg 7730	. 2 ⊢ (∪ 𝐴 ∈ V → ∪ ∪ 𝐴 ∈ V)
3		ssun1 4173	. . . 4 ⊢ dom 𝐴 ⊆ (dom 𝐴 ∪ ran 𝐴)
4		dmrnssfld 5970	. . . 4 ⊢ (dom 𝐴 ∪ ran 𝐴) ⊆ ∪ ∪ 𝐴
5	3, 4	sstri 3992	. . 3 ⊢ dom 𝐴 ⊆ ∪ ∪ 𝐴
6		ssexg 5324	. . 3 ⊢ ((dom 𝐴 ⊆ ∪ ∪ 𝐴 ∧ ∪ ∪ 𝐴 ∈ V) → dom 𝐴 ∈ V)
7	5, 6	mpan 689	. 2 ⊢ (∪ ∪ 𝐴 ∈ V → dom 𝐴 ∈ V)
8	1, 2, 7	3syl 18	1 ⊢ (𝐴 ∈ 𝑉 → dom 𝐴 ∈ V)

Syntax hints:   → wi 4   ∈ wcel 2107  Vcvv 3475   ∪ cun 3947   ⊆ wss 3949  ∪ cuni 4909  dom cdm 5677  ran crn 5678

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-sep 5300  ax-nul 5307  ax-pr 5428  ax-un 7725

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-opab 5212  df-cnv 5685  df-dm 5687  df-rn 5688

This theorem is referenced by:  dmexd  7896  dmfex  7898  dmex  7902  iprc  7904  exse2  7908  xpexr2  7910  xpexcnv  7911  soex  7912  cnvexg  7915  coexg  7920  cofunexg  7935  offval3  7969  opabn1stprc  8044  suppval  8148  funsssuppss  8175  suppssOLD  8180  suppssov1  8183  suppssfv  8187  tposexg  8225  tfrlem12  8389  tfrlem13  8390  erexb  8728  f1vrnfibi  9337  oion  9531  ttrclexg  9718  fpwwe2lem3  10628  hashfn  14335  hashfundm  14402  hashf1dmrn  14403  fundmge2nop0  14453  fun2dmnop0  14455  trclexlem  14941  relexp0g  14969  relexpsucnnr  14972  o1of2  15557  isofn  17722  ssclem  17766  ssc2  17769  ssctr  17772  subsubc  17803  resf1st  17844  resf2nd  17845  funcres  17846  dprddomprc  19870  dprdval0prc  19872  subgdmdprd  19904  dprd2da  19912  decpmatval0  22266  pmatcollpw3lem  22285  ordtbaslem  22692  ordtuni  22694  ordtbas2  22695  ordtbas  22696  ordttopon  22697  ordtopn1  22698  ordtopn2  22699  txindislem  23137  ordthmeolem  23305  ptcmplem2  23557  tuslem  23771  tuslemOLD  23772  dvnff  25440  bdayval  27151  noextend  27169  bdayfo  27180  vtxdgf  28728  fdifsuppconst  31911  ressupprn  31912  ofcfval3  33100  braew  33240  omsval  33292  sibfof  33339  sitmcl  33350  cndprobval  33432  tailf  35260  tailfb  35262  ismgmOLD  36718  dfcnvrefrels2  37398  dfcnvrefrels3  37399  rclexi  42366  rtrclexlem  42367  cnvrcl0  42376  dfrtrcl5  42380  relexpmulg  42461  relexp01min  42464  relexpxpmin  42468  unidmex  43737  caragenval  45209  caragenunidm  45224  itcoval0  47348  itcoval1  47349