Theorem dmexg 7843

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 7685	. 2 ⊢ (𝐴 ∈ 𝑉 → ∪ 𝐴 ∈ V)
2		uniexg 7685	. 2 ⊢ (∪ 𝐴 ∈ V → ∪ ∪ 𝐴 ∈ V)
3		ssun1 4130	. . . 4 ⊢ dom 𝐴 ⊆ (dom 𝐴 ∪ ran 𝐴)
4		dmrnssfld 5923	. . . 4 ⊢ (dom 𝐴 ∪ ran 𝐴) ⊆ ∪ ∪ 𝐴
5	3, 4	sstri 3943	. . 3 ⊢ dom 𝐴 ⊆ ∪ ∪ 𝐴
6		ssexg 5268	. . 3 ⊢ ((dom 𝐴 ⊆ ∪ ∪ 𝐴 ∧ ∪ ∪ 𝐴 ∈ V) → dom 𝐴 ∈ V)
7	5, 6	mpan 690	. 2 ⊢ (∪ ∪ 𝐴 ∈ V → dom 𝐴 ∈ V)
8	1, 2, 7	3syl 18	1 ⊢ (𝐴 ∈ 𝑉 → dom 𝐴 ∈ V)

Syntax hints:   → wi 4   ∈ wcel 2113  Vcvv 3440   ∪ cun 3899   ⊆ wss 3901  ∪ cuni 4863  dom cdm 5624  ran crn 5625

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pr 5377  ax-un 7680

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-opab 5161  df-cnv 5632  df-dm 5634  df-rn 5635

This theorem is referenced by:  dmexd  7845  dmfex  7847  dmex  7851  iprc  7853  exse2  7859  xpexr2  7861  xpexcnv  7862  soex  7863  cnvexg  7866  coexg  7871  cofunexg  7893  offval3  7926  opabn1stprc  8002  suppval  8104  funsssuppss  8132  suppssov1  8139  suppssov2  8140  suppssfv  8144  tposexg  8182  tfrlem12  8320  tfrlem13  8321  erexb  8660  f1vrnfibi  9242  oion  9441  ttrclexg  9632  fpwwe2lem3  10544  hashfn  14298  hashfundm  14365  hashf1dmrn  14366  fundmge2nop0  14425  fun2dmnop0  14427  trclexlem  14917  relexp0g  14945  relexpsucnnr  14948  o1of2  15536  isofn  17699  ssclem  17743  ssc2  17746  ssctr  17749  subsubc  17777  resf1st  17818  resf2nd  17819  funcres  17820  dprddomprc  19931  dprdval0prc  19933  subgdmdprd  19965  dprd2da  19973  decpmatval0  22708  pmatcollpw3lem  22727  ordtbaslem  23132  ordtuni  23134  ordtbas2  23135  ordtbas  23136  ordttopon  23137  ordtopn1  23138  ordtopn2  23139  txindislem  23577  ordthmeolem  23745  ptcmplem2  23997  tuslem  24210  dvnff  25881  bdayval  27616  noextend  27634  bdayfo  27645  vtxdgf  29545  fdifsuppconst  32768  ressupprn  32769  ofcfval3  34259  braew  34399  omsval  34450  sibfof  34497  sitmcl  34508  cndprobval  34590  tailf  36569  tailfb  36571  ismgmOLD  38051  dfcnvrefrels2  38781  dfcnvrefrels3  38782  rclexi  43856  rtrclexlem  43857  cnvrcl0  43866  dfrtrcl5  43870  relexpmulg  43951  relexp01min  43954  relexpxpmin  43958  unidmex  45295  caragenval  46737  caragenunidm  46752  itcoval0  48908  itcoval1  48909  isofnALT  49276