Theorem dmexg 7877

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 7718	. 2 ⊢ (𝐴 ∈ 𝑉 → ∪ 𝐴 ∈ V)
2		uniexg 7718	. 2 ⊢ (∪ 𝐴 ∈ V → ∪ ∪ 𝐴 ∈ V)
3		ssun1 4128	. . . 4 ⊢ dom 𝐴 ⊆ (dom 𝐴 ∪ ran 𝐴)
4		dmrnssfld 5946	. . . 4 ⊢ (dom 𝐴 ∪ ran 𝐴) ⊆ ∪ ∪ 𝐴
5	3, 4	sstri 3943	. . 3 ⊢ dom 𝐴 ⊆ ∪ ∪ 𝐴
6		ssexg 5276	. . 3 ⊢ ((dom 𝐴 ⊆ ∪ ∪ 𝐴 ∧ ∪ ∪ 𝐴 ∈ V) → dom 𝐴 ∈ V)
7	5, 6	mpan 700	. 2 ⊢ (∪ ∪ 𝐴 ∈ V → dom 𝐴 ∈ V)
8	1, 2, 7	3syl 18	1 ⊢ (𝐴 ∈ 𝑉 → dom 𝐴 ∈ V)

Syntax hints:   → wi 4   ∈ wcel 2141  Vcvv 3453   ∪ cun 3900   ⊆ wss 3902  ∪ cuni 4862  dom cdm 5643  ran crn 5644

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733  ax-sep 5243  ax-pr 5387  ax-un 7713

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3455  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4284  df-if 4478  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4863  df-br 5098  df-opab 5160  df-cnv 5651  df-dm 5653  df-rn 5654

This theorem is referenced by:  dmexd  7879  dmfex  7881  dmex  7885  iprc  7887  exse2  7893  xpexr2  7895  xpexcnv  7896  soex  7897  cnvexg  7900  coexg  7905  cofunexg  7925  offval3  7958  opabn1stprc  8034  suppval  8136  funsssuppss  8164  suppssov1  8171  suppssov2  8172  suppssfv  8176  tposexg  8214  tfrlem12  8354  tfrlem13  8355  erexb  8698  f1vrnfibi  9279  oion  9478  ttrclexg  9672  fpwwe2lem3  10585  hashfn  14382  hashfundm  14449  hashf1dmrn  14450  fundmge2nop0  14509  fun2dmnop0  14511  trclexlem  15001  relexp0g  15029  relexpsucnnr  15032  o1of2  15631  isofn  17799  ssclem  17843  ssc2  17846  ssctr  17849  subsubc  17877  resf1st  17918  resf2nd  17919  funcres  17920  dprddomprc  20033  dprdval0prc  20035  subgdmdprd  20067  dprd2da  20075  decpmatval0  22812  pmatcollpw3lem  22831  ordtbaslem  23236  ordtuni  23238  ordtbas2  23239  ordtbas  23240  ordttopon  23241  ordtopn1  23242  ordtopn2  23243  txindislem  23681  ordthmeolem  23849  ptcmplem2  24101  tuslem  24314  dvnff  25973  bdayval  27700  noextend  27718  bdayfo  27729  vtxdgf  29629  fdifsuppconst  32852  ressupprn  32853  ofcfval3  34360  braew  34500  omsval  34551  sibfof  34598  sitmcl  34609  cndprobval  34691  tailf  36696  tailfb  36698  ismgmOLD  38310  dmqsex  38822  qmapex  38911  dfcnvrefrels2  39068  dfcnvrefrels3  39069  rclexi  44152  rtrclexlem  44153  cnvrcl0  44162  dfrtrcl5  44166  relexpmulg  44247  relexp01min  44250  relexpxpmin  44254  unidmex  45591  caragenval  47028  caragenunidm  47043  itcoval0  49245  itcoval1  49246  isofnALT  49613