Theorem dmexg 7895

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 7732	. 2 ⊢ (𝐴 ∈ 𝑉 → ∪ 𝐴 ∈ V)
2		uniexg 7732	. 2 ⊢ (∪ 𝐴 ∈ V → ∪ ∪ 𝐴 ∈ V)
3		ssun1 4153	. . . 4 ⊢ dom 𝐴 ⊆ (dom 𝐴 ∪ ran 𝐴)
4		dmrnssfld 5953	. . . 4 ⊢ (dom 𝐴 ∪ ran 𝐴) ⊆ ∪ ∪ 𝐴
5	3, 4	sstri 3968	. . 3 ⊢ dom 𝐴 ⊆ ∪ ∪ 𝐴
6		ssexg 5293	. . 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 2108  Vcvv 3459   ∪ cun 3924   ⊆ wss 3926  ∪ cuni 4883  dom cdm 5654  ran crn 5655

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pr 5402  ax-un 7727

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-opab 5182  df-cnv 5662  df-dm 5664  df-rn 5665

This theorem is referenced by:  dmexd  7897  dmfex  7899  dmex  7903  iprc  7905  exse2  7911  xpexr2  7913  xpexcnv  7914  soex  7915  cnvexg  7918  coexg  7923  cofunexg  7945  offval3  7979  opabn1stprc  8055  suppval  8159  funsssuppss  8187  suppssov1  8194  suppssov2  8195  suppssfv  8199  tposexg  8237  tfrlem12  8401  tfrlem13  8402  erexb  8742  f1vrnfibi  9352  oion  9548  ttrclexg  9735  fpwwe2lem3  10645  hashfn  14391  hashfundm  14458  hashf1dmrn  14459  fundmge2nop0  14518  fun2dmnop0  14520  trclexlem  15011  relexp0g  15039  relexpsucnnr  15042  o1of2  15627  isofn  17786  ssclem  17830  ssc2  17833  ssctr  17836  subsubc  17864  resf1st  17905  resf2nd  17906  funcres  17907  dprddomprc  19981  dprdval0prc  19983  subgdmdprd  20015  dprd2da  20023  decpmatval0  22700  pmatcollpw3lem  22719  ordtbaslem  23124  ordtuni  23126  ordtbas2  23127  ordtbas  23128  ordttopon  23129  ordtopn1  23130  ordtopn2  23131  txindislem  23569  ordthmeolem  23737  ptcmplem2  23989  tuslem  24203  dvnff  25875  bdayval  27610  noextend  27628  bdayfo  27639  vtxdgf  29397  fdifsuppconst  32612  ressupprn  32613  ofcfval3  34079  braew  34219  omsval  34271  sibfof  34318  sitmcl  34329  cndprobval  34411  tailf  36339  tailfb  36341  ismgmOLD  37820  dfcnvrefrels2  38492  dfcnvrefrels3  38493  rclexi  43586  rtrclexlem  43587  cnvrcl0  43596  dfrtrcl5  43600  relexpmulg  43681  relexp01min  43684  relexpxpmin  43688  unidmex  45022  caragenval  46470  caragenunidm  46485  itcoval0  48590  itcoval1  48591  isofnALT  48949