Theorem dmexg 7911

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 7755	. 2 ⊢ (𝐴 ∈ 𝑉 → ∪ 𝐴 ∈ V)
2		uniexg 7755	. 2 ⊢ (∪ 𝐴 ∈ V → ∪ ∪ 𝐴 ∈ V)
3		ssun1 4124	. . . 4 ⊢ dom 𝐴 ⊆ (dom 𝐴 ∪ ran 𝐴)
4		dmrnssfld 5956	. . . 4 ⊢ (dom 𝐴 ∪ ran 𝐴) ⊆ ∪ ∪ 𝐴
5	3, 4	sstri 3940	. . 3 ⊢ dom 𝐴 ⊆ ∪ ∪ 𝐴
6		ssexg 5281	. . 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 2145  Vcvv 3451   ∪ cun 3897   ⊆ wss 3899  ∪ cuni 4867  dom cdm 5651  ran crn 5652

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 2147  ax-9 2155  ax-ext 2733  ax-sep 5249  ax-pr 5391  ax-un 7749

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 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-cnv 5659  df-dm 5661  df-rn 5662

This theorem is used by:  dmexd  7913  dmfex  7915  dmex  7919  iprc  7921  exse2  7927  xpexr2  7929  xpexcnv  7930  soex  7931  cnvexg  7934  coexg  7939  cofunexg  7959  offval3  7992  opabn1stprc  8067  suppval  8172  funsssuppss  8200  suppssov1  8207  suppssov2  8208  suppssfv  8212  tposexg  8250  tfrlem12  8390  tfrlem13  8391  erexb  8736  f1vrnfibi  9324  oion  9523  ttrclexg  9717  fpwwe2lem3  10711  hashfn  14512  hashfundm  14580  hashf1dmrn  14581  fundmge2nop0  14640  fun2dmnop0  14642  trclexlem  15140  relexp0g  15168  relexpsucnnr  15171  o1of2  15773  isofn  17943  ssclem  17987  ssc2  17990  ssctr  17993  subsubc  18021  resf1st  18062  resf2nd  18063  funcres  18064  dprddomprc  20209  dprdval0prc  20211  subgdmdprd  20243  dprd2da  20251  decpmatval0  23075  pmatcollpw3lem  23094  ordtbaslem  23499  ordtuni  23501  ordtbas2  23502  ordtbas  23503  ordttopon  23504  ordtopn1  23505  ordtopn2  23506  txindislem  23945  ordthmeolem  24113  ptcmplem2  24365  tuslem  24578  dvnff  26236  bdayval  27998  noextend  28016  bdayfo  28027  vtxdgf  30045  fdifsuppconst  33275  ressupprn  33276  ofcfval3  34727  braew  34868  omsval  34918  sibfof  34965  sitmcl  34976  cndprobval  35058  tailf  37143  tailfb  37145  ismgmOLD  38764  dmqsex  39274  qmapex  39363  dfcnvrefrels2  39520  dfcnvrefrels3  39521  rclexi  44600  rtrclexlem  44601  cnvrcl0  44610  dfrtrcl5  44614  relexpmulg  44695  relexp01min  44698  relexpxpmin  44702  unidmex  46036  caragenval  47472  caragenunidm  47487  itcoval0  49743  itcoval1  49744  isofnALT  50108