Theorem dmexg 6989

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 6853	. 2 ⊢ (𝐴 ∈ 𝑉 → ∪ 𝐴 ∈ V)
2		uniexg 6853	. 2 ⊢ (∪ 𝐴 ∈ V → ∪ ∪ 𝐴 ∈ V)
3		ssun1 3738	. . . 4 ⊢ dom 𝐴 ⊆ (dom 𝐴 ∪ ran 𝐴)
4		dmrnssfld 5305	. . . 4 ⊢ (dom 𝐴 ∪ ran 𝐴) ⊆ ∪ ∪ 𝐴
5	3, 4	sstri 3577	. . 3 ⊢ dom 𝐴 ⊆ ∪ ∪ 𝐴
6		ssexg 4732	. . 3 ⊢ ((dom 𝐴 ⊆ ∪ ∪ 𝐴 ∧ ∪ ∪ 𝐴 ∈ V) → dom 𝐴 ∈ V)
7	5, 6	mpan 702	. 2 ⊢ (∪ ∪ 𝐴 ∈ V → dom 𝐴 ∈ V)
8	1, 2, 7	3syl 18	1 ⊢ (𝐴 ∈ 𝑉 → dom 𝐴 ∈ V)

Syntax hints:   → wi 4   ∈ wcel 1977  Vcvv 3173   ∪ cun 3538   ⊆ wss 3540  ∪ cuni 4372  dom cdm 5038  ran crn 5039

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pr 4833  ax-un 6847

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rex 2902  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-br 4584  df-opab 4644  df-cnv 5046  df-dm 5048  df-rn 5049

This theorem is referenced by:  dmex  6991  iprc  6993  exse2  6998  xpexr2  7000  xpexcnv  7001  soex  7002  cnvexg  7005  coexg  7010  dmfex  7017  cofunexg  7023  offval3  7053  suppval  7184  funsssuppss  7208  suppss  7212  suppssov1  7214  suppssfv  7218  tposexg  7253  tfrlem12  7372  tfrlem13  7373  erexb  7654  f1vrnfibi  8134  oion  8324  unxpwdom2  8376  wemapwe  8477  imadomg  9237  fpwwe2lem3  9334  fpwwe2lem12  9342  fpwwe2lem13  9343  hashfn  13025  fundmge2nop0  13129  fun2dmnop0  13131  trclexlem  13581  relexp0g  13610  relexpsucnnr  13613  o1of2  14191  prdsplusg  15941  prdsmulr  15942  prdsvsca  15943  prdshom  15950  isofn  16258  ssclem  16302  ssc2  16305  ssctr  16308  subsubc  16336  resf1st  16377  resf2nd  16378  funcres  16379  efgrcl  17951  dprddomprc  18222  dprdval0prc  18224  dprdgrp  18227  dprdf  18228  dprdssv  18238  subgdmdprd  18256  dprd2da  18264  f1lindf  19980  decpmatval0  20388  pmatcollpw3lem  20407  ordtbaslem  20802  ordtuni  20804  ordtbas2  20805  ordtbas  20806  ordttopon  20807  ordtopn1  20808  ordtopn2  20809  ordtrest2lem  20817  ordtrest2  20818  txindislem  21246  ordthmeolem  21414  ptcmplem2  21667  tuslem  21881  mbfmulc2re  23221  mbfneg  23223  dvnff  23492  dchrptlem3  24791  structgrssvtxlem  25700  fiusgraedgfi  25936  sizeusglecusg  26014  wlks  26047  wlkres  26050  trls  26066  crcts  26150  cycls  26151  vdusgraval  26434  vdgrnn0pnf  26436  hashnbgravdg  26440  usgravd0nedg  26445  iseupa  26492  vdgn0frgrav2  26551  vdgn1frgrav2  26553  vdgfrgragt2  26554  gsummpt2d  29112  ofcfval3  29491  braew  29632  omsval  29682  sibfof  29729  sitmcl  29740  cndprobval  29822  bdayval  31045  bdayfo  31074  tailf  31540  tailfb  31542  ismgmOLD  32819  rclexi  36941  rtrclexlem  36942  trclubgNEW  36944  cnvrcl0  36951  dfrtrcl5  36955  relexpmulg  37021  relexp01min  37024  relexpxpmin  37028  unidmex  38242  dmexd  38417  caragenval  39383  omecl  39393  caragenunidm  39398  opabn1stprc  40318  vtxdgf  40686  offval0  42093