Theorem dmexg 7899

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 7740	. 2 ⊢ (𝐴 ∈ 𝑉 → ∪ 𝐴 ∈ V)
2		uniexg 7740	. 2 ⊢ (∪ 𝐴 ∈ V → ∪ ∪ 𝐴 ∈ V)
3		ssun1 4132	. . . 4 ⊢ dom 𝐴 ⊆ (dom 𝐴 ∪ ran 𝐴)
4		dmrnssfld 5966	. . . 4 ⊢ (dom 𝐴 ∪ ran 𝐴) ⊆ ∪ ∪ 𝐴
5	3, 4	sstri 3947	. . 3 ⊢ dom 𝐴 ⊆ ∪ ∪ 𝐴
6		ssexg 5291	. . 3 ⊢ ((dom 𝐴 ⊆ ∪ ∪ 𝐴 ∧ ∪ ∪ 𝐴 ∈ V) → dom 𝐴 ∈ V)
7	5, 6	mpan 702	. 2 ⊢ (∪ ∪ 𝐴 ∈ V → dom 𝐴 ∈ V)
8	1, 2, 7	3syl 19	1 ⊢ (𝐴 ∈ 𝑉 → dom 𝐴 ∈ V)

Syntax hints:   → wi 4   ∈ wcel 2143  Vcvv 3455   ∪ cun 3904   ⊆ wss 3906  ∪ cuni 4873  dom cdm 5663  ran crn 5664

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-sep 5258  ax-pr 5406  ax-un 7734

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-v 3457  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4489  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4874  df-br 5111  df-opab 5175  df-cnv 5671  df-dm 5673  df-rn 5674

This theorem is referenced by:  dmexd  7901  dmfex  7903  dmex  7907  iprc  7909  exse2  7915  xpexr2  7917  xpexcnv  7918  soex  7919  cnvexg  7922  coexg  7927  cofunexg  7947  offval3  7980  opabn1stprc  8056  suppval  8159  funsssuppss  8187  suppssov1  8194  suppssov2  8195  suppssfv  8199  tposexg  8237  tfrlem12  8377  tfrlem13  8378  erexb  8721  f1vrnfibi  9300  oion  9499  ttrclexg  9693  fpwwe2lem3  10619  hashfn  14413  hashfundm  14481  hashf1dmrn  14482  fundmge2nop0  14541  fun2dmnop0  14543  trclexlem  15033  relexp0g  15061  relexpsucnnr  15064  o1of2  15666  isofn  17833  ssclem  17877  ssc2  17880  ssctr  17883  subsubc  17911  resf1st  17952  resf2nd  17953  funcres  17954  dprddomprc  20073  dprdval0prc  20075  subgdmdprd  20107  dprd2da  20115  decpmatval0  22902  pmatcollpw3lem  22921  ordtbaslem  23326  ordtuni  23328  ordtbas2  23329  ordtbas  23330  ordttopon  23331  ordtopn1  23332  ordtopn2  23333  txindislem  23771  ordthmeolem  23939  ptcmplem2  24191  tuslem  24404  dvnff  26063  bdayval  27793  noextend  27811  bdayfo  27822  vtxdgf  29802  fdifsuppconst  33015  ressupprn  33016  ofcfval3  34473  braew  34613  omsval  34664  sibfof  34711  sitmcl  34722  cndprobval  34804  tailf  36867  tailfb  36869  ismgmOLD  38482  dmqsex  38992  qmapex  39081  dfcnvrefrels2  39238  dfcnvrefrels3  39239  rclexi  44324  rtrclexlem  44325  cnvrcl0  44334  dfrtrcl5  44338  relexpmulg  44419  relexp01min  44422  relexpxpmin  44426  unidmex  45753  caragenval  47190  caragenunidm  47205  itcoval0  49425  itcoval1  49426  isofnALT  49792