Theorem dmexg 7737

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 7584	. 2 ⊢ (𝐴 ∈ 𝑉 → ∪ 𝐴 ∈ V)
2		uniexg 7584	. 2 ⊢ (∪ 𝐴 ∈ V → ∪ ∪ 𝐴 ∈ V)
3		ssun1 4110	. . . 4 ⊢ dom 𝐴 ⊆ (dom 𝐴 ∪ ran 𝐴)
4		dmrnssfld 5876	. . . 4 ⊢ (dom 𝐴 ∪ ran 𝐴) ⊆ ∪ ∪ 𝐴
5	3, 4	sstri 3934	. . 3 ⊢ dom 𝐴 ⊆ ∪ ∪ 𝐴
6		ssexg 5250	. . 3 ⊢ ((dom 𝐴 ⊆ ∪ ∪ 𝐴 ∧ ∪ ∪ 𝐴 ∈ V) → dom 𝐴 ∈ V)
7	5, 6	mpan 686	. 2 ⊢ (∪ ∪ 𝐴 ∈ V → dom 𝐴 ∈ V)
8	1, 2, 7	3syl 18	1 ⊢ (𝐴 ∈ 𝑉 → dom 𝐴 ∈ V)

Syntax hints:   → wi 4   ∈ wcel 2109  Vcvv 3430   ∪ cun 3889   ⊆ wss 3891  ∪ cuni 4844  dom cdm 5588  ran crn 5589

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-ext 2710  ax-sep 5226  ax-nul 5233  ax-pr 5355  ax-un 7579

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1544  df-fal 1554  df-ex 1786  df-sb 2071  df-clab 2717  df-cleq 2731  df-clel 2817  df-rab 3074  df-v 3432  df-dif 3894  df-un 3896  df-in 3898  df-ss 3908  df-nul 4262  df-if 4465  df-sn 4567  df-pr 4569  df-op 4573  df-uni 4845  df-br 5079  df-opab 5141  df-cnv 5596  df-dm 5598  df-rn 5599

This theorem is referenced by:  dmexd  7739  dmfex  7741  dmex  7745  iprc  7747  exse2  7751  xpexr2  7753  xpexcnv  7754  soex  7755  cnvexg  7758  coexg  7763  cofunexg  7778  offval3  7811  opabn1stprc  7884  suppval  7963  funsssuppss  7990  suppssOLD  7995  suppssov1  7998  suppssfv  8002  tposexg  8040  tfrlem12  8204  tfrlem13  8205  erexb  8497  f1vrnfibi  9065  oion  9256  ttrclexg  9442  fpwwe2lem3  10373  hashfn  14071  fundmge2nop0  14187  fun2dmnop0  14189  trclexlem  14686  relexp0g  14714  relexpsucnnr  14717  o1of2  15303  isofn  17468  ssclem  17512  ssc2  17515  ssctr  17518  subsubc  17549  resf1st  17590  resf2nd  17591  funcres  17592  dprddomprc  19584  dprdval0prc  19586  subgdmdprd  19618  dprd2da  19626  decpmatval0  21894  pmatcollpw3lem  21913  ordtbaslem  22320  ordtuni  22322  ordtbas2  22323  ordtbas  22324  ordttopon  22325  ordtopn1  22326  ordtopn2  22327  txindislem  22765  ordthmeolem  22933  ptcmplem2  23185  tuslem  23399  tuslemOLD  23400  dvnff  25068  vtxdgf  27819  fdifsuppconst  31002  ressupprn  31003  ofcfval3  32049  braew  32189  omsval  32239  sibfof  32286  sitmcl  32297  cndprobval  32379  hashfundm  33053  hashf1dmrn  33054  bdayval  33830  noextend  33848  bdayfo  33859  tailf  34543  tailfb  34545  ismgmOLD  35987  dfcnvrefrels2  36623  dfcnvrefrels3  36624  rclexi  41176  rtrclexlem  41177  cnvrcl0  41186  dfrtrcl5  41190  relexpmulg  41271  relexp01min  41274  relexpxpmin  41278  unidmex  42551  caragenval  43985  caragenunidm  44000  itcoval0  45960  itcoval1  45961