Theorem dmexg 7941

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 7775	. 2 ⊢ (𝐴 ∈ 𝑉 → ∪ 𝐴 ∈ V)
2		uniexg 7775	. 2 ⊢ (∪ 𝐴 ∈ V → ∪ ∪ 𝐴 ∈ V)
3		ssun1 4201	. . . 4 ⊢ dom 𝐴 ⊆ (dom 𝐴 ∪ ran 𝐴)
4		dmrnssfld 5996	. . . 4 ⊢ (dom 𝐴 ∪ ran 𝐴) ⊆ ∪ ∪ 𝐴
5	3, 4	sstri 4018	. . 3 ⊢ dom 𝐴 ⊆ ∪ ∪ 𝐴
6		ssexg 5341	. . 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 2108  Vcvv 3488   ∪ cun 3974   ⊆ wss 3976  ∪ cuni 4931  dom cdm 5700  ran crn 5701

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pr 5447  ax-un 7770

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-opab 5229  df-cnv 5708  df-dm 5710  df-rn 5711

This theorem is referenced by:  dmexd  7943  dmfex  7945  dmex  7949  iprc  7951  exse2  7957  xpexr2  7959  xpexcnv  7960  soex  7961  cnvexg  7964  coexg  7969  cofunexg  7989  offval3  8023  opabn1stprc  8099  suppval  8203  funsssuppss  8231  suppssov1  8238  suppssov2  8239  suppssfv  8243  tposexg  8281  tfrlem12  8445  tfrlem13  8446  erexb  8788  f1vrnfibi  9410  oion  9605  ttrclexg  9792  fpwwe2lem3  10702  hashfn  14424  hashfundm  14491  hashf1dmrn  14492  fundmge2nop0  14551  fun2dmnop0  14553  trclexlem  15043  relexp0g  15071  relexpsucnnr  15074  o1of2  15659  isofn  17836  ssclem  17880  ssc2  17883  ssctr  17886  subsubc  17917  resf1st  17958  resf2nd  17959  funcres  17960  dprddomprc  20044  dprdval0prc  20046  subgdmdprd  20078  dprd2da  20086  decpmatval0  22791  pmatcollpw3lem  22810  ordtbaslem  23217  ordtuni  23219  ordtbas2  23220  ordtbas  23221  ordttopon  23222  ordtopn1  23223  ordtopn2  23224  txindislem  23662  ordthmeolem  23830  ptcmplem2  24082  tuslem  24296  tuslemOLD  24297  dvnff  25979  bdayval  27711  noextend  27729  bdayfo  27740  vtxdgf  29507  fdifsuppconst  32701  ressupprn  32702  ofcfval3  34066  braew  34206  omsval  34258  sibfof  34305  sitmcl  34316  cndprobval  34398  tailf  36341  tailfb  36343  ismgmOLD  37810  dfcnvrefrels2  38484  dfcnvrefrels3  38485  rclexi  43577  rtrclexlem  43578  cnvrcl0  43587  dfrtrcl5  43591  relexpmulg  43672  relexp01min  43675  relexpxpmin  43679  unidmex  44952  caragenval  46414  caragenunidm  46429  itcoval0  48396  itcoval1  48397