Theorem dmexg 7853

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 7695	. 2 ⊢ (𝐴 ∈ 𝑉 → ∪ 𝐴 ∈ V)
2		uniexg 7695	. 2 ⊢ (∪ 𝐴 ∈ V → ∪ ∪ 𝐴 ∈ V)
3		ssun1 4132	. . . 4 ⊢ dom 𝐴 ⊆ (dom 𝐴 ∪ ran 𝐴)
4		dmrnssfld 5931	. . . 4 ⊢ (dom 𝐴 ∪ ran 𝐴) ⊆ ∪ ∪ 𝐴
5	3, 4	sstri 3945	. . 3 ⊢ dom 𝐴 ⊆ ∪ ∪ 𝐴
6		ssexg 5270	. . 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 3442   ∪ cun 3901   ⊆ wss 3903  ∪ cuni 4865  dom cdm 5632  ran crn 5633

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 2709  ax-sep 5243  ax-pr 5379  ax-un 7690

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 2716  df-cleq 2729  df-clel 2812  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-cnv 5640  df-dm 5642  df-rn 5643

This theorem is referenced by:  dmexd  7855  dmfex  7857  dmex  7861  iprc  7863  exse2  7869  xpexr2  7871  xpexcnv  7872  soex  7873  cnvexg  7876  coexg  7881  cofunexg  7903  offval3  7936  opabn1stprc  8012  suppval  8114  funsssuppss  8142  suppssov1  8149  suppssov2  8150  suppssfv  8154  tposexg  8192  tfrlem12  8330  tfrlem13  8331  erexb  8671  f1vrnfibi  9254  oion  9453  ttrclexg  9644  fpwwe2lem3  10556  hashfn  14310  hashfundm  14377  hashf1dmrn  14378  fundmge2nop0  14437  fun2dmnop0  14439  trclexlem  14929  relexp0g  14957  relexpsucnnr  14960  o1of2  15548  isofn  17711  ssclem  17755  ssc2  17758  ssctr  17761  subsubc  17789  resf1st  17830  resf2nd  17831  funcres  17832  dprddomprc  19943  dprdval0prc  19945  subgdmdprd  19977  dprd2da  19985  decpmatval0  22720  pmatcollpw3lem  22739  ordtbaslem  23144  ordtuni  23146  ordtbas2  23147  ordtbas  23148  ordttopon  23149  ordtopn1  23150  ordtopn2  23151  txindislem  23589  ordthmeolem  23757  ptcmplem2  24009  tuslem  24222  dvnff  25893  bdayval  27628  noextend  27646  bdayfo  27657  vtxdgf  29557  fdifsuppconst  32778  ressupprn  32779  ofcfval3  34279  braew  34419  omsval  34470  sibfof  34517  sitmcl  34528  cndprobval  34610  tailf  36588  tailfb  36590  ismgmOLD  38098  dmqsex  38610  qmapex  38699  dfcnvrefrels2  38856  dfcnvrefrels3  38857  rclexi  43968  rtrclexlem  43969  cnvrcl0  43978  dfrtrcl5  43982  relexpmulg  44063  relexp01min  44066  relexpxpmin  44070  unidmex  45407  caragenval  46848  caragenunidm  46863  itcoval0  49019  itcoval1  49020  isofnALT  49387