Theorem dmexg 7923

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 7760	. 2 ⊢ (𝐴 ∈ 𝑉 → ∪ 𝐴 ∈ V)
2		uniexg 7760	. 2 ⊢ (∪ 𝐴 ∈ V → ∪ ∪ 𝐴 ∈ V)
3		ssun1 4178	. . . 4 ⊢ dom 𝐴 ⊆ (dom 𝐴 ∪ ran 𝐴)
4		dmrnssfld 5984	. . . 4 ⊢ (dom 𝐴 ∪ ran 𝐴) ⊆ ∪ ∪ 𝐴
5	3, 4	sstri 3993	. . 3 ⊢ dom 𝐴 ⊆ ∪ ∪ 𝐴
6		ssexg 5323	. . 3 ⊢ ((dom 𝐴 ⊆ ∪ ∪ 𝐴 ∧ ∪ ∪ 𝐴 ∈ V) → dom 𝐴 ∈ V)
7	5, 6	mpan 690	. 2 ⊢ (∪ ∪ 𝐴 ∈ V → dom 𝐴 ∈ V)
8	1, 2, 7	3syl 18	1 ⊢ (𝐴 ∈ 𝑉 → dom 𝐴 ∈ V)

Syntax hints:   → wi 4   ∈ wcel 2108  Vcvv 3480   ∪ cun 3949   ⊆ wss 3951  ∪ cuni 4907  dom cdm 5685  ran crn 5686

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432  ax-un 7755

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-opab 5206  df-cnv 5693  df-dm 5695  df-rn 5696

This theorem is referenced by:  dmexd  7925  dmfex  7927  dmex  7931  iprc  7933  exse2  7939  xpexr2  7941  xpexcnv  7942  soex  7943  cnvexg  7946  coexg  7951  cofunexg  7973  offval3  8007  opabn1stprc  8083  suppval  8187  funsssuppss  8215  suppssov1  8222  suppssov2  8223  suppssfv  8227  tposexg  8265  tfrlem12  8429  tfrlem13  8430  erexb  8770  f1vrnfibi  9382  oion  9576  ttrclexg  9763  fpwwe2lem3  10673  hashfn  14414  hashfundm  14481  hashf1dmrn  14482  fundmge2nop0  14541  fun2dmnop0  14543  trclexlem  15033  relexp0g  15061  relexpsucnnr  15064  o1of2  15649  isofn  17819  ssclem  17863  ssc2  17866  ssctr  17869  subsubc  17898  resf1st  17939  resf2nd  17940  funcres  17941  dprddomprc  20020  dprdval0prc  20022  subgdmdprd  20054  dprd2da  20062  decpmatval0  22770  pmatcollpw3lem  22789  ordtbaslem  23196  ordtuni  23198  ordtbas2  23199  ordtbas  23200  ordttopon  23201  ordtopn1  23202  ordtopn2  23203  txindislem  23641  ordthmeolem  23809  ptcmplem2  24061  tuslem  24275  tuslemOLD  24276  dvnff  25959  bdayval  27693  noextend  27711  bdayfo  27722  vtxdgf  29489  fdifsuppconst  32698  ressupprn  32699  ofcfval3  34103  braew  34243  omsval  34295  sibfof  34342  sitmcl  34353  cndprobval  34435  tailf  36376  tailfb  36378  ismgmOLD  37857  dfcnvrefrels2  38529  dfcnvrefrels3  38530  rclexi  43628  rtrclexlem  43629  cnvrcl0  43638  dfrtrcl5  43642  relexpmulg  43723  relexp01min  43726  relexpxpmin  43730  unidmex  45055  caragenval  46508  caragenunidm  46523  itcoval0  48583  itcoval1  48584