Theorem dmexg 7358

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 7215	. 2 ⊢ (𝐴 ∈ 𝑉 → ∪ 𝐴 ∈ V)
2		uniexg 7215	. 2 ⊢ (∪ 𝐴 ∈ V → ∪ ∪ 𝐴 ∈ V)
3		ssun1 4003	. . . 4 ⊢ dom 𝐴 ⊆ (dom 𝐴 ∪ ran 𝐴)
4		dmrnssfld 5617	. . . 4 ⊢ (dom 𝐴 ∪ ran 𝐴) ⊆ ∪ ∪ 𝐴
5	3, 4	sstri 3836	. . 3 ⊢ dom 𝐴 ⊆ ∪ ∪ 𝐴
6		ssexg 5029	. . 3 ⊢ ((dom 𝐴 ⊆ ∪ ∪ 𝐴 ∧ ∪ ∪ 𝐴 ∈ V) → dom 𝐴 ∈ V)
7	5, 6	mpan 683	. 2 ⊢ (∪ ∪ 𝐴 ∈ V → dom 𝐴 ∈ V)
8	1, 2, 7	3syl 18	1 ⊢ (𝐴 ∈ 𝑉 → dom 𝐴 ∈ V)

Syntax hints:   → wi 4   ∈ wcel 2166  Vcvv 3414   ∪ cun 3796   ⊆ wss 3798  ∪ cuni 4658  dom cdm 5342  ran crn 5343

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-8 2168  ax-9 2175  ax-10 2194  ax-11 2209  ax-12 2222  ax-13 2391  ax-ext 2803  ax-sep 5005  ax-nul 5013  ax-pr 5127  ax-un 7209

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-3an 1115  df-tru 1662  df-ex 1881  df-nf 1885  df-sb 2070  df-mo 2605  df-eu 2640  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-rex 3123  df-rab 3126  df-v 3416  df-dif 3801  df-un 3803  df-in 3805  df-ss 3812  df-nul 4145  df-if 4307  df-sn 4398  df-pr 4400  df-op 4404  df-uni 4659  df-br 4874  df-opab 4936  df-cnv 5350  df-dm 5352  df-rn 5353

This theorem is referenced by:  dmexd  7360  dmex  7361  iprc  7363  exse2  7367  xpexr2  7369  xpexcnv  7370  soex  7371  cnvexg  7374  coexg  7379  dmfex  7386  cofunexg  7392  offval3  7422  opabn1stprc  7490  suppval  7561  funsssuppss  7586  suppss  7590  suppssov1  7592  suppssfv  7596  tposexg  7631  tfrlem12  7751  tfrlem13  7752  erexb  8034  f1vrnfibi  8520  oion  8710  fpwwe2lem3  9770  hashfn  13454  fundmge2nop0  13563  fun2dmnop0  13565  trclexlem  14112  relexp0g  14139  relexpsucnnr  14142  o1of2  14720  isofn  16787  ssclem  16831  ssc2  16834  ssctr  16837  subsubc  16865  resf1st  16906  resf2nd  16907  funcres  16908  dprddomprc  18753  dprdval0prc  18755  subgdmdprd  18787  dprd2da  18795  decpmatval0  20939  pmatcollpw3lem  20958  ordtbaslem  21363  ordtuni  21365  ordtbas2  21366  ordtbas  21367  ordttopon  21368  ordtopn1  21369  ordtopn2  21370  txindislem  21807  ordthmeolem  21975  ptcmplem2  22227  tuslem  22441  dvnff  24085  vtxdgf  26769  ofcfval3  30709  braew  30850  omsval  30900  sibfof  30947  sitmcl  30958  cndprobval  31041  bdayval  32340  noextend  32358  bdayfo  32367  tailf  32908  tailfb  32910  ismgmOLD  34191  dfcnvrefrels2  34824  dfcnvrefrels3  34825  rclexi  38763  rtrclexlem  38764  cnvrcl0  38773  dfrtrcl5  38777  relexpmulg  38843  relexp01min  38846  relexpxpmin  38850  unidmex  40034  caragenval  41501  caragenunidm  41516  offval0  43146