Theorem dmexg 7890

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 7726	. 2 ⊢ (𝐴 ∈ 𝑉 → ∪ 𝐴 ∈ V)
2		uniexg 7726	. 2 ⊢ (∪ 𝐴 ∈ V → ∪ ∪ 𝐴 ∈ V)
3		ssun1 4171	. . . 4 ⊢ dom 𝐴 ⊆ (dom 𝐴 ∪ ran 𝐴)
4		dmrnssfld 5967	. . . 4 ⊢ (dom 𝐴 ∪ ran 𝐴) ⊆ ∪ ∪ 𝐴
5	3, 4	sstri 3990	. . 3 ⊢ dom 𝐴 ⊆ ∪ ∪ 𝐴
6		ssexg 5322	. . 3 ⊢ ((dom 𝐴 ⊆ ∪ ∪ 𝐴 ∧ ∪ ∪ 𝐴 ∈ V) → dom 𝐴 ∈ V)
7	5, 6	mpan 688	. 2 ⊢ (∪ ∪ 𝐴 ∈ V → dom 𝐴 ∈ V)
8	1, 2, 7	3syl 18	1 ⊢ (𝐴 ∈ 𝑉 → dom 𝐴 ∈ V)

Syntax hints:   → wi 4   ∈ wcel 2106  Vcvv 3474   ∪ cun 3945   ⊆ wss 3947  ∪ cuni 4907  dom cdm 5675  ran crn 5676

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703  ax-sep 5298  ax-nul 5305  ax-pr 5426  ax-un 7721

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-rab 3433  df-v 3476  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-opab 5210  df-cnv 5683  df-dm 5685  df-rn 5686

This theorem is referenced by:  dmexd  7892  dmfex  7894  dmex  7898  iprc  7900  exse2  7904  xpexr2  7906  xpexcnv  7907  soex  7908  cnvexg  7911  coexg  7916  cofunexg  7931  offval3  7965  opabn1stprc  8040  suppval  8144  funsssuppss  8171  suppssOLD  8176  suppssov1  8179  suppssfv  8183  tposexg  8221  tfrlem12  8385  tfrlem13  8386  erexb  8724  f1vrnfibi  9333  oion  9527  ttrclexg  9714  fpwwe2lem3  10624  hashfn  14331  hashfundm  14398  hashf1dmrn  14399  fundmge2nop0  14449  fun2dmnop0  14451  trclexlem  14937  relexp0g  14965  relexpsucnnr  14968  o1of2  15553  isofn  17718  ssclem  17762  ssc2  17765  ssctr  17768  subsubc  17799  resf1st  17840  resf2nd  17841  funcres  17842  dprddomprc  19864  dprdval0prc  19866  subgdmdprd  19898  dprd2da  19906  decpmatval0  22257  pmatcollpw3lem  22276  ordtbaslem  22683  ordtuni  22685  ordtbas2  22686  ordtbas  22687  ordttopon  22688  ordtopn1  22689  ordtopn2  22690  txindislem  23128  ordthmeolem  23296  ptcmplem2  23548  tuslem  23762  tuslemOLD  23763  dvnff  25431  bdayval  27140  noextend  27158  bdayfo  27169  vtxdgf  28717  fdifsuppconst  31898  ressupprn  31899  ofcfval3  33088  braew  33228  omsval  33280  sibfof  33327  sitmcl  33338  cndprobval  33420  tailf  35248  tailfb  35250  ismgmOLD  36706  dfcnvrefrels2  37386  dfcnvrefrels3  37387  rclexi  42351  rtrclexlem  42352  cnvrcl0  42361  dfrtrcl5  42365  relexpmulg  42446  relexp01min  42449  relexpxpmin  42453  unidmex  43722  caragenval  45195  caragenunidm  45210  itcoval0  47301  itcoval1  47302