Theorem dmexg 7900

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 7744	. 2 ⊢ (𝐴 ∈ 𝑉 → ∪ 𝐴 ∈ V)
2		uniexg 7744	. 2 ⊢ (∪ 𝐴 ∈ V → ∪ ∪ 𝐴 ∈ V)
3		ssun1 4131	. . . 4 ⊢ dom 𝐴 ⊆ (dom 𝐴 ∪ ran 𝐴)
4		dmrnssfld 5966	. . . 4 ⊢ (dom 𝐴 ∪ ran 𝐴) ⊆ ∪ ∪ 𝐴
5	3, 4	sstri 3947	. . 3 ⊢ dom 𝐴 ⊆ ∪ ∪ 𝐴
6		ssexg 5292	. . 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 2146  Vcvv 3457   ∪ cun 3904   ⊆ wss 3906  ∪ cuni 4874  dom cdm 5663  ran crn 5664

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737  ax-sep 5259  ax-pr 5406  ax-un 7738

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-opab 5176  df-cnv 5671  df-dm 5673  df-rn 5674

This theorem is used by:  dmexd  7902  dmfex  7904  dmex  7908  iprc  7910  exse2  7916  xpexr2  7918  xpexcnv  7919  soex  7920  cnvexg  7923  coexg  7928  cofunexg  7948  offval3  7981  opabn1stprc  8057  suppval  8160  funsssuppss  8188  suppssov1  8195  suppssov2  8196  suppssfv  8200  tposexg  8238  tfrlem12  8378  tfrlem13  8379  erexb  8722  f1vrnfibi  9302  oion  9501  ttrclexg  9695  fpwwe2lem3  10629  hashfn  14424  hashfundm  14492  hashf1dmrn  14493  fundmge2nop0  14552  fun2dmnop0  14554  trclexlem  15050  relexp0g  15078  relexpsucnnr  15081  o1of2  15683  isofn  17849  ssclem  17893  ssc2  17896  ssctr  17899  subsubc  17927  resf1st  17968  resf2nd  17969  funcres  17970  dprddomprc  20095  dprdval0prc  20097  subgdmdprd  20129  dprd2da  20137  decpmatval0  22950  pmatcollpw3lem  22969  ordtbaslem  23374  ordtuni  23376  ordtbas2  23377  ordtbas  23378  ordttopon  23379  ordtopn1  23380  ordtopn2  23381  txindislem  23819  ordthmeolem  23987  ptcmplem2  24239  tuslem  24452  dvnff  26111  bdayval  27841  noextend  27859  bdayfo  27870  vtxdgf  29850  fdifsuppconst  33063  ressupprn  33064  ofcfval3  34515  braew  34656  omsval  34707  sibfof  34754  sitmcl  34765  cndprobval  34847  tailf  36919  tailfb  36921  ismgmOLD  38534  dmqsex  39044  qmapex  39133  dfcnvrefrels2  39290  dfcnvrefrels3  39291  rclexi  44374  rtrclexlem  44375  cnvrcl0  44384  dfrtrcl5  44388  relexpmulg  44469  relexp01min  44472  relexpxpmin  44476  unidmex  45803  caragenval  47240  caragenunidm  47255  itcoval0  49475  itcoval1  49476  isofnALT  49842