Theorem dmexg 7894

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 7735	. 2 ⊢ (𝐴 ∈ 𝑉 → ∪ 𝐴 ∈ V)
2		uniexg 7735	. 2 ⊢ (∪ 𝐴 ∈ V → ∪ ∪ 𝐴 ∈ V)
3		ssun1 4139	. . . 4 ⊢ dom 𝐴 ⊆ (dom 𝐴 ∪ ran 𝐴)
4		dmrnssfld 5962	. . . 4 ⊢ (dom 𝐴 ∪ ran 𝐴) ⊆ ∪ ∪ 𝐴
5	3, 4	sstri 3954	. . 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 2149  Vcvv 3463   ∪ cun 3911   ⊆ wss 3913  ∪ cuni 4873  dom cdm 5659  ran crn 5660

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741  ax-sep 5258  ax-pr 5402  ax-un 7730

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4874  df-br 5111  df-opab 5175  df-cnv 5667  df-dm 5669  df-rn 5670

This theorem is referenced by:  dmexd  7896  dmfex  7898  dmex  7902  iprc  7904  exse2  7910  xpexr2  7912  xpexcnv  7913  soex  7914  cnvexg  7917  coexg  7922  cofunexg  7942  offval3  7975  opabn1stprc  8051  suppval  8154  funsssuppss  8182  suppssov1  8189  suppssov2  8190  suppssfv  8194  tposexg  8232  tfrlem12  8372  tfrlem13  8373  erexb  8716  f1vrnfibi  9295  oion  9494  ttrclexg  9688  fpwwe2lem3  10614  hashfn  14407  hashfundm  14475  hashf1dmrn  14476  fundmge2nop0  14535  fun2dmnop0  14537  trclexlem  15027  relexp0g  15055  relexpsucnnr  15058  o1of2  15660  isofn  17828  ssclem  17872  ssc2  17875  ssctr  17878  subsubc  17906  resf1st  17947  resf2nd  17948  funcres  17949  dprddomprc  20068  dprdval0prc  20070  subgdmdprd  20102  dprd2da  20110  decpmatval0  22886  pmatcollpw3lem  22905  ordtbaslem  23310  ordtuni  23312  ordtbas2  23313  ordtbas  23314  ordttopon  23315  ordtopn1  23316  ordtopn2  23317  txindislem  23755  ordthmeolem  23923  ptcmplem2  24175  tuslem  24388  dvnff  26047  bdayval  27774  noextend  27792  bdayfo  27803  vtxdgf  29758  fdifsuppconst  32971  ressupprn  32972  ofcfval3  34433  braew  34573  omsval  34624  sibfof  34671  sitmcl  34682  cndprobval  34764  tailf  36771  tailfb  36773  ismgmOLD  38384  dmqsex  38896  qmapex  38985  dfcnvrefrels2  39142  dfcnvrefrels3  39143  rclexi  44226  rtrclexlem  44227  cnvrcl0  44236  dfrtrcl5  44240  relexpmulg  44321  relexp01min  44324  relexpxpmin  44328  unidmex  45655  caragenval  47092  caragenunidm  47107  itcoval0  49320  itcoval1  49321  isofnALT  49687