Theorem dmexg 7750

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 7593	. 2 ⊢ (𝐴 ∈ 𝑉 → ∪ 𝐴 ∈ V)
2		uniexg 7593	. 2 ⊢ (∪ 𝐴 ∈ V → ∪ ∪ 𝐴 ∈ V)
3		ssun1 4106	. . . 4 ⊢ dom 𝐴 ⊆ (dom 𝐴 ∪ ran 𝐴)
4		dmrnssfld 5879	. . . 4 ⊢ (dom 𝐴 ∪ ran 𝐴) ⊆ ∪ ∪ 𝐴
5	3, 4	sstri 3930	. . 3 ⊢ dom 𝐴 ⊆ ∪ ∪ 𝐴
6		ssexg 5247	. . 3 ⊢ ((dom 𝐴 ⊆ ∪ ∪ 𝐴 ∧ ∪ ∪ 𝐴 ∈ V) → dom 𝐴 ∈ V)
7	5, 6	mpan 687	. 2 ⊢ (∪ ∪ 𝐴 ∈ V → dom 𝐴 ∈ V)
8	1, 2, 7	3syl 18	1 ⊢ (𝐴 ∈ 𝑉 → dom 𝐴 ∈ V)

Syntax hints:   → wi 4   ∈ wcel 2106  Vcvv 3432   ∪ cun 3885   ⊆ wss 3887  ∪ cuni 4839  dom cdm 5589  ran crn 5590

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709  ax-sep 5223  ax-nul 5230  ax-pr 5352  ax-un 7588

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-rab 3073  df-v 3434  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-br 5075  df-opab 5137  df-cnv 5597  df-dm 5599  df-rn 5600

This theorem is referenced by:  dmexd  7752  dmfex  7754  dmex  7758  iprc  7760  exse2  7764  xpexr2  7766  xpexcnv  7767  soex  7768  cnvexg  7771  coexg  7776  cofunexg  7791  offval3  7825  opabn1stprc  7898  suppval  7979  funsssuppss  8006  suppssOLD  8011  suppssov1  8014  suppssfv  8018  tposexg  8056  tfrlem12  8220  tfrlem13  8221  erexb  8523  f1vrnfibi  9104  oion  9295  ttrclexg  9481  fpwwe2lem3  10389  hashfn  14090  fundmge2nop0  14206  fun2dmnop0  14208  trclexlem  14705  relexp0g  14733  relexpsucnnr  14736  o1of2  15322  isofn  17487  ssclem  17531  ssc2  17534  ssctr  17537  subsubc  17568  resf1st  17609  resf2nd  17610  funcres  17611  dprddomprc  19603  dprdval0prc  19605  subgdmdprd  19637  dprd2da  19645  decpmatval0  21913  pmatcollpw3lem  21932  ordtbaslem  22339  ordtuni  22341  ordtbas2  22342  ordtbas  22343  ordttopon  22344  ordtopn1  22345  ordtopn2  22346  txindislem  22784  ordthmeolem  22952  ptcmplem2  23204  tuslem  23418  tuslemOLD  23419  dvnff  25087  vtxdgf  27838  fdifsuppconst  31023  ressupprn  31024  ofcfval3  32070  braew  32210  omsval  32260  sibfof  32307  sitmcl  32318  cndprobval  32400  hashfundm  33074  hashf1dmrn  33075  bdayval  33851  noextend  33869  bdayfo  33880  tailf  34564  tailfb  34566  ismgmOLD  36008  dfcnvrefrels2  36644  dfcnvrefrels3  36645  rclexi  41223  rtrclexlem  41224  cnvrcl0  41233  dfrtrcl5  41237  relexpmulg  41318  relexp01min  41321  relexpxpmin  41325  unidmex  42598  caragenval  44031  caragenunidm  44046  itcoval0  46008  itcoval1  46009