Theorem dmexg 7945

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 7787	. 2 ⊢ (𝐴 ∈ 𝑉 → ∪ 𝐴 ∈ V)
2		uniexg 7787	. 2 ⊢ (∪ 𝐴 ∈ V → ∪ ∪ 𝐴 ∈ V)
3		ssun1 4179	. . . 4 ⊢ dom 𝐴 ⊆ (dom 𝐴 ∪ ran 𝐴)
4		dmrnssfld 5966	. . . 4 ⊢ (dom 𝐴 ∪ ran 𝐴) ⊆ ∪ ∪ 𝐴
5	3, 4	sstri 3922	. . 3 ⊢ dom 𝐴 ⊆ ∪ ∪ 𝐴
6		ssexg 5286	. . 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 2147  Vcvv 3454   ⊆ wss 3900   ∪ cun 4152  ∪ cuni 4870  dom cdm 5656  ran crn 5657

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-sep 5253  ax-pr 5396  ax-un 7781

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 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-opab 5172  df-cnv 5664  df-dm 5666  df-rn 5667

This theorem is used by:  dmexd  7947  dmfex  7949  dmex  7953  iprc  7955  exse2  7961  xpexr2  7963  xpexcnv  7964  soex  7965  cnvexg  7968  coexg  7973  cofunexg  7993  offval3  8026  opabn1stprc  8102  suppval  8214  funsssuppss  8243  suppssov1  8250  suppssov2  8251  suppssfv  8255  tposexg  8293  tfrlem12  8433  tfrlem13  8434  erexb  8779  f1vrnfibi  9367  oion  9565  ttrclexg  9759  fpwwe2lem3  10755  hashfn  14558  hashfundm  14626  hashf1dmrn  14627  fundmge2nop0  14686  fun2dmnop0  14688  trclexlem  15188  relexp0g  15216  relexpsucnnr  15219  o1of2  15821  isofn  17991  ssclem  18035  ssc2  18038  ssctr  18041  subsubc  18069  resf1st  18110  resf2nd  18111  funcres  18112  dprddomprc  20258  dprdval0prc  20260  subgdmdprd  20292  dprd2da  20300  decpmatval0  23126  pmatcollpw3lem  23145  ordtbaslem  23550  ordtuni  23552  ordtbas2  23553  ordtbas  23554  ordttopon  23555  ordtopn1  23556  ordtopn2  23557  txindislem  23996  ordthmeolem  24164  ptcmplem2  24416  tuslem  24629  dvnff  26287  bdayval  28051  noextend  28069  bdayfo  28080  vtxdgf  30098  fdifsuppconst  33369  ressupprn  33370  ofcfval3  34838  braew  34979  omsval  35029  omssubadd  35036  sibfof  35076  sitmcl  35087  cndprobval  35169  tailf  37371  tailfb  37373  ismgmOLD  39043  dmqsex  39553  qmapex  39642  dfcnvrefrels2  39799  dfcnvrefrels3  39800  rclexi  44870  rtrclexlem  44871  cnvrcl0  44880  dfrtrcl5  44884  relexpmulg  44965  relexp01min  44968  relexpxpmin  44972  unidmex  46335  caragenval  47770  caragenunidm  47785  itcoval0  50099  itcoval1  50100  isofnALT  50470