Theorem dmexg 7913

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 7749	. 2 ⊢ (𝐴 ∈ 𝑉 → ∪ 𝐴 ∈ V)
2		uniexg 7749	. 2 ⊢ (∪ 𝐴 ∈ V → ∪ ∪ 𝐴 ∈ V)
3		ssun1 4172	. . . 4 ⊢ dom 𝐴 ⊆ (dom 𝐴 ∪ ran 𝐴)
4		dmrnssfld 5975	. . . 4 ⊢ (dom 𝐴 ∪ ran 𝐴) ⊆ ∪ ∪ 𝐴
5	3, 4	sstri 3989	. . 3 ⊢ dom 𝐴 ⊆ ∪ ∪ 𝐴
6		ssexg 5325	. . 3 ⊢ ((dom 𝐴 ⊆ ∪ ∪ 𝐴 ∧ ∪ ∪ 𝐴 ∈ V) → dom 𝐴 ∈ V)
7	5, 6	mpan 688	. 2 ⊢ (∪ ∪ 𝐴 ∈ V → dom 𝐴 ∈ V)
8	1, 2, 7	3syl 18	1 ⊢ (𝐴 ∈ 𝑉 → dom 𝐴 ∈ V)

Syntax hints:   → wi 4   ∈ wcel 2098  Vcvv 3471   ∪ cun 3945   ⊆ wss 3947  ∪ cuni 4910  dom cdm 5680  ran crn 5681

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2698  ax-sep 5301  ax-nul 5308  ax-pr 5431  ax-un 7744

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2705  df-cleq 2719  df-clel 2805  df-rab 3429  df-v 3473  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4325  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4911  df-br 5151  df-opab 5213  df-cnv 5688  df-dm 5690  df-rn 5691

This theorem is referenced by:  dmexd  7915  dmfex  7917  dmex  7921  iprc  7923  exse2  7929  xpexr2  7931  xpexcnv  7932  soex  7933  cnvexg  7936  coexg  7941  cofunexg  7956  offval3  7990  opabn1stprc  8066  suppval  8171  funsssuppss  8199  suppssOLD  8204  suppssov1  8207  suppssov2  8208  suppssfv  8212  tposexg  8250  tfrlem12  8414  tfrlem13  8415  erexb  8754  f1vrnfibi  9367  oion  9565  ttrclexg  9752  fpwwe2lem3  10662  hashfn  14372  hashfundm  14439  hashf1dmrn  14440  fundmge2nop0  14491  fun2dmnop0  14493  trclexlem  14979  relexp0g  15007  relexpsucnnr  15010  o1of2  15595  isofn  17763  ssclem  17807  ssc2  17810  ssctr  17813  subsubc  17844  resf1st  17885  resf2nd  17886  funcres  17887  dprddomprc  19962  dprdval0prc  19964  subgdmdprd  19996  dprd2da  20004  decpmatval0  22684  pmatcollpw3lem  22703  ordtbaslem  23110  ordtuni  23112  ordtbas2  23113  ordtbas  23114  ordttopon  23115  ordtopn1  23116  ordtopn2  23117  txindislem  23555  ordthmeolem  23723  ptcmplem2  23975  tuslem  24189  tuslemOLD  24190  dvnff  25871  bdayval  27599  noextend  27617  bdayfo  27628  vtxdgf  29303  fdifsuppconst  32487  ressupprn  32488  ofcfval3  33726  braew  33866  omsval  33918  sibfof  33965  sitmcl  33976  cndprobval  34058  tailf  35864  tailfb  35866  ismgmOLD  37328  dfcnvrefrels2  38004  dfcnvrefrels3  38005  rclexi  43048  rtrclexlem  43049  cnvrcl0  43058  dfrtrcl5  43062  relexpmulg  43143  relexp01min  43146  relexpxpmin  43150  unidmex  44417  caragenval  45883  caragenunidm  45898  itcoval0  47786  itcoval1  47787