Theorem dmexg 7845

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 7687	. 2 ⊢ (𝐴 ∈ 𝑉 → ∪ 𝐴 ∈ V)
2		uniexg 7687	. 2 ⊢ (∪ 𝐴 ∈ V → ∪ ∪ 𝐴 ∈ V)
3		ssun1 4119	. . . 4 ⊢ dom 𝐴 ⊆ (dom 𝐴 ∪ ran 𝐴)
4		dmrnssfld 5923	. . . 4 ⊢ (dom 𝐴 ∪ ran 𝐴) ⊆ ∪ ∪ 𝐴
5	3, 4	sstri 3932	. . 3 ⊢ dom 𝐴 ⊆ ∪ ∪ 𝐴
6		ssexg 5260	. . 3 ⊢ ((dom 𝐴 ⊆ ∪ ∪ 𝐴 ∧ ∪ ∪ 𝐴 ∈ V) → dom 𝐴 ∈ V)
7	5, 6	mpan 691	. 2 ⊢ (∪ ∪ 𝐴 ∈ V → dom 𝐴 ∈ V)
8	1, 2, 7	3syl 18	1 ⊢ (𝐴 ∈ 𝑉 → dom 𝐴 ∈ V)

Syntax hints:   → wi 4   ∈ wcel 2114  Vcvv 3430   ∪ cun 3888   ⊆ wss 3890  ∪ cuni 4851  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 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5231  ax-pr 5370  ax-un 7682

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-cnv 5632  df-dm 5634  df-rn 5635

This theorem is referenced by:  dmexd  7847  dmfex  7849  dmex  7853  iprc  7855  exse2  7861  xpexr2  7863  xpexcnv  7864  soex  7865  cnvexg  7868  coexg  7873  cofunexg  7895  offval3  7928  opabn1stprc  8004  suppval  8105  funsssuppss  8133  suppssov1  8140  suppssov2  8141  suppssfv  8145  tposexg  8183  tfrlem12  8321  tfrlem13  8322  erexb  8662  f1vrnfibi  9245  oion  9444  ttrclexg  9635  fpwwe2lem3  10547  hashfn  14328  hashfundm  14395  hashf1dmrn  14396  fundmge2nop0  14455  fun2dmnop0  14457  trclexlem  14947  relexp0g  14975  relexpsucnnr  14978  o1of2  15566  isofn  17733  ssclem  17777  ssc2  17780  ssctr  17783  subsubc  17811  resf1st  17852  resf2nd  17853  funcres  17854  dprddomprc  19968  dprdval0prc  19970  subgdmdprd  20002  dprd2da  20010  decpmatval0  22739  pmatcollpw3lem  22758  ordtbaslem  23163  ordtuni  23165  ordtbas2  23166  ordtbas  23167  ordttopon  23168  ordtopn1  23169  ordtopn2  23170  txindislem  23608  ordthmeolem  23776  ptcmplem2  24028  tuslem  24241  dvnff  25900  bdayval  27626  noextend  27644  bdayfo  27655  vtxdgf  29555  fdifsuppconst  32777  ressupprn  32778  ofcfval3  34262  braew  34402  omsval  34453  sibfof  34500  sitmcl  34511  cndprobval  34593  tailf  36573  tailfb  36575  ismgmOLD  38185  dmqsex  38697  qmapex  38786  dfcnvrefrels2  38943  dfcnvrefrels3  38944  rclexi  44060  rtrclexlem  44061  cnvrcl0  44070  dfrtrcl5  44074  relexpmulg  44155  relexp01min  44158  relexpxpmin  44162  unidmex  45499  caragenval  46939  caragenunidm  46954  itcoval0  49150  itcoval1  49151  isofnALT  49518