Theorem dmexg 7857

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 7696	. 2 ⊢ (𝐴 ∈ 𝑉 → ∪ 𝐴 ∈ V)
2		uniexg 7696	. 2 ⊢ (∪ 𝐴 ∈ V → ∪ ∪ 𝐴 ∈ V)
3		ssun1 4137	. . . 4 ⊢ dom 𝐴 ⊆ (dom 𝐴 ∪ ran 𝐴)
4		dmrnssfld 5926	. . . 4 ⊢ (dom 𝐴 ∪ ran 𝐴) ⊆ ∪ ∪ 𝐴
5	3, 4	sstri 3953	. . 3 ⊢ dom 𝐴 ⊆ ∪ ∪ 𝐴
6		ssexg 5273	. . 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 2109  Vcvv 3444   ∪ cun 3909   ⊆ wss 3911  ∪ cuni 4867  dom cdm 5631  ran crn 5632

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5246  ax-nul 5256  ax-pr 5382  ax-un 7691

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3403  df-v 3446  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5103  df-opab 5165  df-cnv 5639  df-dm 5641  df-rn 5642

This theorem is referenced by:  dmexd  7859  dmfex  7861  dmex  7865  iprc  7867  exse2  7873  xpexr2  7875  xpexcnv  7876  soex  7877  cnvexg  7880  coexg  7885  cofunexg  7907  offval3  7940  opabn1stprc  8016  suppval  8118  funsssuppss  8146  suppssov1  8153  suppssov2  8154  suppssfv  8158  tposexg  8196  tfrlem12  8334  tfrlem13  8335  erexb  8673  f1vrnfibi  9269  oion  9465  ttrclexg  9652  fpwwe2lem3  10562  hashfn  14316  hashfundm  14383  hashf1dmrn  14384  fundmge2nop0  14443  fun2dmnop0  14445  trclexlem  14936  relexp0g  14964  relexpsucnnr  14967  o1of2  15555  isofn  17713  ssclem  17757  ssc2  17760  ssctr  17763  subsubc  17791  resf1st  17832  resf2nd  17833  funcres  17834  dprddomprc  19908  dprdval0prc  19910  subgdmdprd  19942  dprd2da  19950  decpmatval0  22627  pmatcollpw3lem  22646  ordtbaslem  23051  ordtuni  23053  ordtbas2  23054  ordtbas  23055  ordttopon  23056  ordtopn1  23057  ordtopn2  23058  txindislem  23496  ordthmeolem  23664  ptcmplem2  23916  tuslem  24130  dvnff  25801  bdayval  27536  noextend  27554  bdayfo  27565  vtxdgf  29375  fdifsuppconst  32585  ressupprn  32586  ofcfval3  34065  braew  34205  omsval  34257  sibfof  34304  sitmcl  34315  cndprobval  34397  tailf  36336  tailfb  36338  ismgmOLD  37817  dfcnvrefrels2  38492  dfcnvrefrels3  38493  rclexi  43577  rtrclexlem  43578  cnvrcl0  43587  dfrtrcl5  43591  relexpmulg  43672  relexp01min  43675  relexpxpmin  43679  unidmex  45017  caragenval  46464  caragenunidm  46479  itcoval0  48624  itcoval1  48625  isofnALT  48993