Theorem dmexg 7914

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 7758	. 2 ⊢ (𝐴 ∈ 𝑉 → ∪ 𝐴 ∈ V)
2		uniexg 7758	. 2 ⊢ (∪ 𝐴 ∈ V → ∪ ∪ 𝐴 ∈ V)
3		ssun1 4176	. . . 4 ⊢ dom 𝐴 ⊆ (dom 𝐴 ∪ ran 𝐴)
4		dmrnssfld 5955	. . . 4 ⊢ (dom 𝐴 ∪ ran 𝐴) ⊆ ∪ ∪ 𝐴
5	3, 4	sstri 3917	. . 3 ⊢ dom 𝐴 ⊆ ∪ ∪ 𝐴
6		ssexg 5280	. . 3 ⊢ ((dom 𝐴 ⊆ ∪ ∪ 𝐴 ∧ ∪ ∪ 𝐴 ∈ V) → dom 𝐴 ∈ V)
7	5, 6	mpan 703	. 2 ⊢ (∪ ∪ 𝐴 ∈ V → dom 𝐴 ∈ V)
8	1, 2, 7	3syl 19	1 ⊢ (𝐴 ∈ 𝑉 → dom 𝐴 ∈ V)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144  Vcvv 3450   ⊆ wss 3895   ∪ cun 4149  ∪ cuni 4866  dom cdm 5650  ran crn 5651

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248  ax-pr 5390  ax-un 7752

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-opab 5167  df-cnv 5658  df-dm 5660  df-rn 5661

This theorem is used by:  dmexd  7916  dmfex  7918  dmex  7922  iprc  7924  exse2  7930  xpexr2  7932  xpexcnv  7933  soex  7934  cnvexg  7937  coexg  7942  cofunexg  7962  offval3  7995  opabn1stprc  8070  suppval  8182  funsssuppss  8211  suppssov1  8218  suppssov2  8219  suppssfv  8223  tposexg  8261  tfrlem12  8401  tfrlem13  8402  erexb  8747  f1vrnfibi  9335  oion  9534  ttrclexg  9728  fpwwe2lem3  10722  hashfn  14523  hashfundm  14591  hashf1dmrn  14592  fundmge2nop0  14651  fun2dmnop0  14653  trclexlem  15153  relexp0g  15181  relexpsucnnr  15184  o1of2  15786  isofn  17956  ssclem  18000  ssc2  18003  ssctr  18006  subsubc  18034  resf1st  18075  resf2nd  18076  funcres  18077  dprddomprc  20222  dprdval0prc  20224  subgdmdprd  20256  dprd2da  20264  decpmatval0  23088  pmatcollpw3lem  23107  ordtbaslem  23512  ordtuni  23514  ordtbas2  23515  ordtbas  23516  ordttopon  23517  ordtopn1  23518  ordtopn2  23519  txindislem  23958  ordthmeolem  24126  ptcmplem2  24378  tuslem  24591  dvnff  26249  bdayval  28011  noextend  28029  bdayfo  28040  vtxdgf  30058  fdifsuppconst  33330  ressupprn  33331  ofcfval3  34781  braew  34922  omsval  34972  omssubadd  34979  sibfof  35019  sitmcl  35030  cndprobval  35112  tailf  37256  tailfb  37258  ismgmOLD  38878  dmqsex  39388  qmapex  39477  dfcnvrefrels2  39634  dfcnvrefrels3  39635  rclexi  44709  rtrclexlem  44710  cnvrcl0  44719  dfrtrcl5  44723  relexpmulg  44804  relexp01min  44807  relexpxpmin  44811  unidmex  46161  caragenval  47597  caragenunidm  47612  itcoval0  49868  itcoval1  49869  isofnALT  50239