Theorem dmexg 7097

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 6955	. 2 ⊢ (𝐴 ∈ 𝑉 → ∪ 𝐴 ∈ V)
2		uniexg 6955	. 2 ⊢ (∪ 𝐴 ∈ V → ∪ ∪ 𝐴 ∈ V)
3		ssun1 3776	. . . 4 ⊢ dom 𝐴 ⊆ (dom 𝐴 ∪ ran 𝐴)
4		dmrnssfld 5384	. . . 4 ⊢ (dom 𝐴 ∪ ran 𝐴) ⊆ ∪ ∪ 𝐴
5	3, 4	sstri 3612	. . 3 ⊢ dom 𝐴 ⊆ ∪ ∪ 𝐴
6		ssexg 4804	. . 3 ⊢ ((dom 𝐴 ⊆ ∪ ∪ 𝐴 ∧ ∪ ∪ 𝐴 ∈ V) → dom 𝐴 ∈ V)
7	5, 6	mpan 706	. 2 ⊢ (∪ ∪ 𝐴 ∈ V → dom 𝐴 ∈ V)
8	1, 2, 7	3syl 18	1 ⊢ (𝐴 ∈ 𝑉 → dom 𝐴 ∈ V)

Syntax hints:   → wi 4   ∈ wcel 1990  Vcvv 3200   ∪ cun 3572   ⊆ wss 3574  ∪ cuni 4436  dom cdm 5114  ran crn 5115

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pr 4906  ax-un 6949

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-rex 2918  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-opab 4713  df-cnv 5122  df-dm 5124  df-rn 5125

This theorem is referenced by:  dmex  7099  iprc  7101  exse2  7105  xpexr2  7107  xpexcnv  7108  soex  7109  cnvexg  7112  coexg  7117  dmfex  7124  cofunexg  7130  offval3  7162  opabn1stprc  7228  suppval  7297  funsssuppss  7321  suppss  7325  suppssov1  7327  suppssfv  7331  tposexg  7366  tfrlem12  7485  tfrlem13  7486  erexb  7767  f1vrnfibi  8251  oion  8441  unxpwdom2  8493  wemapwe  8594  imadomg  9356  fpwwe2lem3  9455  fpwwe2lem12  9463  fpwwe2lem13  9464  hashfn  13164  hashdmpropge2  13265  fundmge2nop0  13274  fun2dmnop0  13276  trclexlem  13733  relexp0g  13762  relexpsucnnr  13765  o1of2  14343  prdsplusg  16118  prdsmulr  16119  prdsvsca  16120  prdshom  16127  isofn  16435  ssclem  16479  ssc2  16482  ssctr  16485  subsubc  16513  resf1st  16554  resf2nd  16555  funcres  16556  efgrcl  18128  dprddomprc  18399  dprdval0prc  18401  dprdgrp  18404  dprdf  18405  dprdssv  18415  subgdmdprd  18433  dprd2da  18441  f1lindf  20161  decpmatval0  20569  pmatcollpw3lem  20588  ordtbaslem  20992  ordtuni  20994  ordtbas2  20995  ordtbas  20996  ordttopon  20997  ordtopn1  20998  ordtopn2  20999  ordtrest2lem  21007  ordtrest2  21008  txindislem  21436  ordthmeolem  21604  ptcmplem2  21857  tuslem  22071  mbfmulc2re  23415  mbfneg  23417  dvnff  23686  dchrptlem3  24991  structgrssvtxlemOLD  25915  vtxdgf  26367  gsummpt2d  29781  ofcfval3  30164  braew  30305  omsval  30355  sibfof  30402  sitmcl  30413  cndprobval  30495  bdayval  31801  noextend  31819  bdayfo  31828  tailf  32370  tailfb  32372  ismgmOLD  33649  rclexi  37922  rtrclexlem  37923  trclubgNEW  37925  cnvrcl0  37932  dfrtrcl5  37936  relexpmulg  38002  relexp01min  38005  relexpxpmin  38009  unidmex  39217  dmexd  39422  caragenval  40707  omecl  40717  caragenunidm  40722  offval0  42299