Theorem dmexg 7594

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 7446	. 2 ⊢ (𝐴 ∈ 𝑉 → ∪ 𝐴 ∈ V)
2		uniexg 7446	. 2 ⊢ (∪ 𝐴 ∈ V → ∪ ∪ 𝐴 ∈ V)
3		ssun1 4099	. . . 4 ⊢ dom 𝐴 ⊆ (dom 𝐴 ∪ ran 𝐴)
4		dmrnssfld 5806	. . . 4 ⊢ (dom 𝐴 ∪ ran 𝐴) ⊆ ∪ ∪ 𝐴
5	3, 4	sstri 3924	. . 3 ⊢ dom 𝐴 ⊆ ∪ ∪ 𝐴
6		ssexg 5191	. . 3 ⊢ ((dom 𝐴 ⊆ ∪ ∪ 𝐴 ∧ ∪ ∪ 𝐴 ∈ V) → dom 𝐴 ∈ V)
7	5, 6	mpan 689	. 2 ⊢ (∪ ∪ 𝐴 ∈ V → dom 𝐴 ∈ V)
8	1, 2, 7	3syl 18	1 ⊢ (𝐴 ∈ 𝑉 → dom 𝐴 ∈ V)

Syntax hints:   → wi 4   ∈ wcel 2111  Vcvv 3441   ∪ cun 3879   ⊆ wss 3881  ∪ cuni 4800  dom cdm 5519  ran crn 5520

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5167  ax-nul 5174  ax-pr 5295  ax-un 7441

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-rab 3115  df-v 3443  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4244  df-if 4426  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4801  df-br 5031  df-opab 5093  df-cnv 5527  df-dm 5529  df-rn 5530

This theorem is referenced by:  dmexd  7596  dmex  7598  iprc  7600  exse2  7604  xpexr2  7606  xpexcnv  7607  soex  7608  cnvexg  7611  coexg  7616  dmfex  7623  cofunexg  7632  offval3  7665  opabn1stprc  7738  suppval  7815  funsssuppss  7839  suppss  7843  suppssov1  7845  suppssfv  7849  tposexg  7889  tfrlem12  8008  tfrlem13  8009  erexb  8297  f1vrnfibi  8793  oion  8984  fpwwe2lem3  10044  hashfn  13732  fundmge2nop0  13846  fun2dmnop0  13848  trclexlem  14345  relexp0g  14373  relexpsucnnr  14376  o1of2  14961  isofn  17037  ssclem  17081  ssc2  17084  ssctr  17087  subsubc  17115  resf1st  17156  resf2nd  17157  funcres  17158  dprddomprc  19115  dprdval0prc  19117  subgdmdprd  19149  dprd2da  19157  decpmatval0  21369  pmatcollpw3lem  21388  ordtbaslem  21793  ordtuni  21795  ordtbas2  21796  ordtbas  21797  ordttopon  21798  ordtopn1  21799  ordtopn2  21800  txindislem  22238  ordthmeolem  22406  ptcmplem2  22658  tuslem  22873  dvnff  24526  vtxdgf  27261  suppiniseg  30446  fdifsuppconst  30449  ressupprn  30450  ofcfval3  31471  braew  31611  omsval  31661  sibfof  31708  sitmcl  31719  cndprobval  31801  hashfundm  32464  hashf1dmrn  32465  bdayval  33268  noextend  33286  bdayfo  33295  tailf  33836  tailfb  33838  ismgmOLD  35288  dfcnvrefrels2  35926  dfcnvrefrels3  35927  rclexi  40315  rtrclexlem  40316  cnvrcl0  40325  dfrtrcl5  40329  relexpmulg  40411  relexp01min  40414  relexpxpmin  40418  unidmex  41684  caragenval  43132  caragenunidm  43147  itcoval0  45076  itcoval1  45077