Theorem dmexg 7724

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 7571	. 2 ⊢ (𝐴 ∈ 𝑉 → ∪ 𝐴 ∈ V)
2		uniexg 7571	. 2 ⊢ (∪ 𝐴 ∈ V → ∪ ∪ 𝐴 ∈ V)
3		ssun1 4102	. . . 4 ⊢ dom 𝐴 ⊆ (dom 𝐴 ∪ ran 𝐴)
4		dmrnssfld 5868	. . . 4 ⊢ (dom 𝐴 ∪ ran 𝐴) ⊆ ∪ ∪ 𝐴
5	3, 4	sstri 3926	. . 3 ⊢ dom 𝐴 ⊆ ∪ ∪ 𝐴
6		ssexg 5242	. . 3 ⊢ ((dom 𝐴 ⊆ ∪ ∪ 𝐴 ∧ ∪ ∪ 𝐴 ∈ V) → dom 𝐴 ∈ V)
7	5, 6	mpan 686	. 2 ⊢ (∪ ∪ 𝐴 ∈ V → dom 𝐴 ∈ V)
8	1, 2, 7	3syl 18	1 ⊢ (𝐴 ∈ 𝑉 → dom 𝐴 ∈ V)

Syntax hints:   → wi 4   ∈ wcel 2108  Vcvv 3422   ∪ cun 3881   ⊆ wss 3883  ∪ cuni 4836  dom cdm 5580  ran crn 5581

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pr 5347  ax-un 7566

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-opab 5133  df-cnv 5588  df-dm 5590  df-rn 5591

This theorem is referenced by:  dmexd  7726  dmfex  7728  dmex  7732  iprc  7734  exse2  7738  xpexr2  7740  xpexcnv  7741  soex  7742  cnvexg  7745  coexg  7750  cofunexg  7765  offval3  7798  opabn1stprc  7871  suppval  7950  funsssuppss  7977  suppssOLD  7982  suppssov1  7985  suppssfv  7989  tposexg  8027  tfrlem12  8191  tfrlem13  8192  erexb  8481  f1vrnfibi  9034  oion  9225  fpwwe2lem3  10320  hashfn  14018  fundmge2nop0  14134  fun2dmnop0  14136  trclexlem  14633  relexp0g  14661  relexpsucnnr  14664  o1of2  15250  isofn  17404  ssclem  17448  ssc2  17451  ssctr  17454  subsubc  17484  resf1st  17525  resf2nd  17526  funcres  17527  dprddomprc  19518  dprdval0prc  19520  subgdmdprd  19552  dprd2da  19560  decpmatval0  21821  pmatcollpw3lem  21840  ordtbaslem  22247  ordtuni  22249  ordtbas2  22250  ordtbas  22251  ordttopon  22252  ordtopn1  22253  ordtopn2  22254  txindislem  22692  ordthmeolem  22860  ptcmplem2  23112  tuslem  23326  tuslemOLD  23327  dvnff  24992  vtxdgf  27741  fdifsuppconst  30925  ressupprn  30926  ofcfval3  31970  braew  32110  omsval  32160  sibfof  32207  sitmcl  32218  cndprobval  32300  hashfundm  32974  hashf1dmrn  32975  ttrclexg  33709  bdayval  33778  noextend  33796  bdayfo  33807  tailf  34491  tailfb  34493  ismgmOLD  35935  dfcnvrefrels2  36571  dfcnvrefrels3  36572  rclexi  41112  rtrclexlem  41113  cnvrcl0  41122  dfrtrcl5  41126  relexpmulg  41207  relexp01min  41210  relexpxpmin  41214  unidmex  42487  caragenval  43921  caragenunidm  43936  itcoval0  45896  itcoval1  45897