Theorem dmexg 7852

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 7694	. 2 ⊢ (𝐴 ∈ 𝑉 → ∪ 𝐴 ∈ V)
2		uniexg 7694	. 2 ⊢ (∪ 𝐴 ∈ V → ∪ ∪ 𝐴 ∈ V)
3		ssun1 4118	. . . 4 ⊢ dom 𝐴 ⊆ (dom 𝐴 ∪ ran 𝐴)
4		dmrnssfld 5929	. . . 4 ⊢ (dom 𝐴 ∪ ran 𝐴) ⊆ ∪ ∪ 𝐴
5	3, 4	sstri 3931	. . 3 ⊢ dom 𝐴 ⊆ ∪ ∪ 𝐴
6		ssexg 5264	. . 3 ⊢ ((dom 𝐴 ⊆ ∪ ∪ 𝐴 ∧ ∪ ∪ 𝐴 ∈ V) → dom 𝐴 ∈ V)
7	5, 6	mpan 691	. 2 ⊢ (∪ ∪ 𝐴 ∈ V → dom 𝐴 ∈ V)
8	1, 2, 7	3syl 18	1 ⊢ (𝐴 ∈ 𝑉 → dom 𝐴 ∈ V)

Syntax hints:   → wi 4   ∈ wcel 2114  Vcvv 3429   ∪ cun 3887   ⊆ wss 3889  ∪ cuni 4850  dom cdm 5631  ran crn 5632

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708  ax-sep 5231  ax-pr 5375  ax-un 7689

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-opab 5148  df-cnv 5639  df-dm 5641  df-rn 5642

This theorem is referenced by:  dmexd  7854  dmfex  7856  dmex  7860  iprc  7862  exse2  7868  xpexr2  7870  xpexcnv  7871  soex  7872  cnvexg  7875  coexg  7880  cofunexg  7902  offval3  7935  opabn1stprc  8011  suppval  8112  funsssuppss  8140  suppssov1  8147  suppssov2  8148  suppssfv  8152  tposexg  8190  tfrlem12  8328  tfrlem13  8329  erexb  8669  f1vrnfibi  9252  oion  9451  ttrclexg  9644  fpwwe2lem3  10556  hashfn  14337  hashfundm  14404  hashf1dmrn  14405  fundmge2nop0  14464  fun2dmnop0  14466  trclexlem  14956  relexp0g  14984  relexpsucnnr  14987  o1of2  15575  isofn  17742  ssclem  17786  ssc2  17789  ssctr  17792  subsubc  17820  resf1st  17861  resf2nd  17862  funcres  17863  dprddomprc  19977  dprdval0prc  19979  subgdmdprd  20011  dprd2da  20019  decpmatval0  22729  pmatcollpw3lem  22748  ordtbaslem  23153  ordtuni  23155  ordtbas2  23156  ordtbas  23157  ordttopon  23158  ordtopn1  23159  ordtopn2  23160  txindislem  23598  ordthmeolem  23766  ptcmplem2  24018  tuslem  24231  dvnff  25890  bdayval  27612  noextend  27630  bdayfo  27641  vtxdgf  29540  fdifsuppconst  32762  ressupprn  32763  ofcfval3  34246  braew  34386  omsval  34437  sibfof  34484  sitmcl  34495  cndprobval  34577  tailf  36557  tailfb  36559  ismgmOLD  38171  dmqsex  38683  qmapex  38772  dfcnvrefrels2  38929  dfcnvrefrels3  38930  rclexi  44042  rtrclexlem  44043  cnvrcl0  44052  dfrtrcl5  44056  relexpmulg  44137  relexp01min  44140  relexpxpmin  44144  unidmex  45481  caragenval  46921  caragenunidm  46936  itcoval0  49138  itcoval1  49139  isofnALT  49506