Theorem dmexg 7877

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 7716	. 2 ⊢ (𝐴 ∈ 𝑉 → ∪ 𝐴 ∈ V)
2		uniexg 7716	. 2 ⊢ (∪ 𝐴 ∈ V → ∪ ∪ 𝐴 ∈ V)
3		ssun1 4141	. . . 4 ⊢ dom 𝐴 ⊆ (dom 𝐴 ∪ ran 𝐴)
4		dmrnssfld 5937	. . . 4 ⊢ (dom 𝐴 ∪ ran 𝐴) ⊆ ∪ ∪ 𝐴
5	3, 4	sstri 3956	. . 3 ⊢ dom 𝐴 ⊆ ∪ ∪ 𝐴
6		ssexg 5278	. . 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 3447   ∪ cun 3912   ⊆ wss 3914  ∪ cuni 4871  dom cdm 5638  ran crn 5639

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 5251  ax-nul 5261  ax-pr 5387  ax-un 7711

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 3406  df-v 3449  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-opab 5170  df-cnv 5646  df-dm 5648  df-rn 5649

This theorem is referenced by:  dmexd  7879  dmfex  7881  dmex  7885  iprc  7887  exse2  7893  xpexr2  7895  xpexcnv  7896  soex  7897  cnvexg  7900  coexg  7905  cofunexg  7927  offval3  7961  opabn1stprc  8037  suppval  8141  funsssuppss  8169  suppssov1  8176  suppssov2  8177  suppssfv  8181  tposexg  8219  tfrlem12  8357  tfrlem13  8358  erexb  8696  f1vrnfibi  9293  oion  9489  ttrclexg  9676  fpwwe2lem3  10586  hashfn  14340  hashfundm  14407  hashf1dmrn  14408  fundmge2nop0  14467  fun2dmnop0  14469  trclexlem  14960  relexp0g  14988  relexpsucnnr  14991  o1of2  15579  isofn  17737  ssclem  17781  ssc2  17784  ssctr  17787  subsubc  17815  resf1st  17856  resf2nd  17857  funcres  17858  dprddomprc  19932  dprdval0prc  19934  subgdmdprd  19966  dprd2da  19974  decpmatval0  22651  pmatcollpw3lem  22670  ordtbaslem  23075  ordtuni  23077  ordtbas2  23078  ordtbas  23079  ordttopon  23080  ordtopn1  23081  ordtopn2  23082  txindislem  23520  ordthmeolem  23688  ptcmplem2  23940  tuslem  24154  dvnff  25825  bdayval  27560  noextend  27578  bdayfo  27589  vtxdgf  29399  fdifsuppconst  32612  ressupprn  32613  ofcfval3  34092  braew  34232  omsval  34284  sibfof  34331  sitmcl  34342  cndprobval  34424  tailf  36363  tailfb  36365  ismgmOLD  37844  dfcnvrefrels2  38519  dfcnvrefrels3  38520  rclexi  43604  rtrclexlem  43605  cnvrcl0  43614  dfrtrcl5  43618  relexpmulg  43699  relexp01min  43702  relexpxpmin  43706  unidmex  45044  caragenval  46491  caragenunidm  46506  itcoval0  48651  itcoval1  48652  isofnALT  49020