Theorem dmexg 7898

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 7742	. 2 ⊢ (𝐴 ∈ 𝑉 → ∪ 𝐴 ∈ V)
2		uniexg 7742	. 2 ⊢ (∪ 𝐴 ∈ V → ∪ ∪ 𝐴 ∈ V)
3		ssun1 4124	. . . 4 ⊢ dom 𝐴 ⊆ (dom 𝐴 ∪ ran 𝐴)
4		dmrnssfld 5958	. . . 4 ⊢ (dom 𝐴 ∪ ran 𝐴) ⊆ ∪ ∪ 𝐴
5	3, 4	sstri 3940	. . 3 ⊢ dom 𝐴 ⊆ ∪ ∪ 𝐴
6		ssexg 5284	. . 3 ⊢ ((dom 𝐴 ⊆ ∪ ∪ 𝐴 ∧ ∪ ∪ 𝐴 ∈ V) → dom 𝐴 ∈ V)
7	5, 6	mpan 703	. 2 ⊢ (∪ ∪ 𝐴 ∈ V → dom 𝐴 ∈ V)
8	1, 2, 7	3syl 19	1 ⊢ (𝐴 ∈ 𝑉 → dom 𝐴 ∈ V)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  Vcvv 3450   ∪ cun 3897   ⊆ wss 3899  ∪ cuni 4867  dom cdm 5655  ran crn 5656

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732  ax-sep 5251  ax-pr 5398  ax-un 7736

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-cnv 5663  df-dm 5665  df-rn 5666

This theorem is used by:  dmexd  7900  dmfex  7902  dmex  7906  iprc  7908  exse2  7914  xpexr2  7916  xpexcnv  7917  soex  7918  cnvexg  7921  coexg  7926  cofunexg  7946  offval3  7979  opabn1stprc  8055  suppval  8160  funsssuppss  8188  suppssov1  8195  suppssov2  8196  suppssfv  8200  tposexg  8238  tfrlem12  8378  tfrlem13  8379  erexb  8722  f1vrnfibi  9309  oion  9508  ttrclexg  9702  fpwwe2lem3  10642  hashfn  14439  hashfundm  14507  hashf1dmrn  14508  fundmge2nop0  14567  fun2dmnop0  14569  trclexlem  15067  relexp0g  15095  relexpsucnnr  15098  o1of2  15700  isofn  17864  ssclem  17908  ssc2  17911  ssctr  17914  subsubc  17942  resf1st  17983  resf2nd  17984  funcres  17985  dprddomprc  20129  dprdval0prc  20131  subgdmdprd  20163  dprd2da  20171  decpmatval0  22989  pmatcollpw3lem  23008  ordtbaslem  23413  ordtuni  23415  ordtbas2  23416  ordtbas  23417  ordttopon  23418  ordtopn1  23419  ordtopn2  23420  txindislem  23859  ordthmeolem  24027  ptcmplem2  24279  tuslem  24492  dvnff  26150  bdayval  27884  noextend  27902  bdayfo  27913  vtxdgf  29931  fdifsuppconst  33161  ressupprn  33162  ofcfval3  34612  braew  34753  omsval  34804  sibfof  34851  sitmcl  34862  cndprobval  34944  tailf  36994  tailfb  36996  ismgmOLD  38600  dmqsex  39110  qmapex  39199  dfcnvrefrels2  39356  dfcnvrefrels3  39357  rclexi  44455  rtrclexlem  44456  cnvrcl0  44465  dfrtrcl5  44469  relexpmulg  44550  relexp01min  44553  relexpxpmin  44557  unidmex  45884  caragenval  47321  caragenunidm  47336  itcoval0  49592  itcoval1  49593  isofnALT  49957