Theorem dmexg 7880

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 7719	. 2 ⊢ (𝐴 ∈ 𝑉 → ∪ 𝐴 ∈ V)
2		uniexg 7719	. 2 ⊢ (∪ 𝐴 ∈ V → ∪ ∪ 𝐴 ∈ V)
3		ssun1 4144	. . . 4 ⊢ dom 𝐴 ⊆ (dom 𝐴 ∪ ran 𝐴)
4		dmrnssfld 5940	. . . 4 ⊢ (dom 𝐴 ∪ ran 𝐴) ⊆ ∪ ∪ 𝐴
5	3, 4	sstri 3959	. . 3 ⊢ dom 𝐴 ⊆ ∪ ∪ 𝐴
6		ssexg 5281	. . 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 3450   ∪ cun 3915   ⊆ wss 3917  ∪ cuni 4874  dom cdm 5641  ran crn 5642

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 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390  ax-un 7714

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 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-opab 5173  df-cnv 5649  df-dm 5651  df-rn 5652

This theorem is referenced by:  dmexd  7882  dmfex  7884  dmex  7888  iprc  7890  exse2  7896  xpexr2  7898  xpexcnv  7899  soex  7900  cnvexg  7903  coexg  7908  cofunexg  7930  offval3  7964  opabn1stprc  8040  suppval  8144  funsssuppss  8172  suppssov1  8179  suppssov2  8180  suppssfv  8184  tposexg  8222  tfrlem12  8360  tfrlem13  8361  erexb  8699  f1vrnfibi  9300  oion  9496  ttrclexg  9683  fpwwe2lem3  10593  hashfn  14347  hashfundm  14414  hashf1dmrn  14415  fundmge2nop0  14474  fun2dmnop0  14476  trclexlem  14967  relexp0g  14995  relexpsucnnr  14998  o1of2  15586  isofn  17744  ssclem  17788  ssc2  17791  ssctr  17794  subsubc  17822  resf1st  17863  resf2nd  17864  funcres  17865  dprddomprc  19939  dprdval0prc  19941  subgdmdprd  19973  dprd2da  19981  decpmatval0  22658  pmatcollpw3lem  22677  ordtbaslem  23082  ordtuni  23084  ordtbas2  23085  ordtbas  23086  ordttopon  23087  ordtopn1  23088  ordtopn2  23089  txindislem  23527  ordthmeolem  23695  ptcmplem2  23947  tuslem  24161  dvnff  25832  bdayval  27567  noextend  27585  bdayfo  27596  vtxdgf  29406  fdifsuppconst  32619  ressupprn  32620  ofcfval3  34099  braew  34239  omsval  34291  sibfof  34338  sitmcl  34349  cndprobval  34431  tailf  36370  tailfb  36372  ismgmOLD  37851  dfcnvrefrels2  38526  dfcnvrefrels3  38527  rclexi  43611  rtrclexlem  43612  cnvrcl0  43621  dfrtrcl5  43625  relexpmulg  43706  relexp01min  43709  relexpxpmin  43713  unidmex  45051  caragenval  46498  caragenunidm  46513  itcoval0  48655  itcoval1  48656  isofnALT  49024