MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  dmexg Structured version   Visualization version   GIF version

Theorem dmexg 7841
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
StepHypRef Expression
1 uniexg 7678 . 2 (𝐴𝑉 𝐴 ∈ V)
2 uniexg 7678 . 2 ( 𝐴 ∈ V → 𝐴 ∈ V)
3 ssun1 4133 . . . 4 dom 𝐴 ⊆ (dom 𝐴 ∪ ran 𝐴)
4 dmrnssfld 5926 . . . 4 (dom 𝐴 ∪ ran 𝐴) ⊆ 𝐴
53, 4sstri 3954 . . 3 dom 𝐴 𝐴
6 ssexg 5281 . . 3 ((dom 𝐴 𝐴 𝐴 ∈ V) → dom 𝐴 ∈ V)
75, 6mpan 689 . 2 ( 𝐴 ∈ V → dom 𝐴 ∈ V)
81, 2, 73syl 18 1 (𝐴𝑉 → dom 𝐴 ∈ V)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2107  Vcvv 3444  cun 3909  wss 3911   cuni 4866  dom cdm 5634  ran crn 5635
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-sep 5257  ax-nul 5264  ax-pr 5385  ax-un 7673
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3407  df-v 3446  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4284  df-if 4488  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4867  df-br 5107  df-opab 5169  df-cnv 5642  df-dm 5644  df-rn 5645
This theorem is referenced by:  dmexd  7843  dmfex  7845  dmex  7849  iprc  7851  exse2  7855  xpexr2  7857  xpexcnv  7858  soex  7859  cnvexg  7862  coexg  7867  cofunexg  7882  offval3  7916  opabn1stprc  7991  suppval  8095  funsssuppss  8122  suppssOLD  8127  suppssov1  8130  suppssfv  8134  tposexg  8172  tfrlem12  8336  tfrlem13  8337  erexb  8676  f1vrnfibi  9284  oion  9477  ttrclexg  9664  fpwwe2lem3  10574  hashfn  14281  fundmge2nop0  14397  fun2dmnop0  14399  trclexlem  14885  relexp0g  14913  relexpsucnnr  14916  o1of2  15501  isofn  17663  ssclem  17707  ssc2  17710  ssctr  17713  subsubc  17744  resf1st  17785  resf2nd  17786  funcres  17787  dprddomprc  19784  dprdval0prc  19786  subgdmdprd  19818  dprd2da  19826  decpmatval0  22129  pmatcollpw3lem  22148  ordtbaslem  22555  ordtuni  22557  ordtbas2  22558  ordtbas  22559  ordttopon  22560  ordtopn1  22561  ordtopn2  22562  txindislem  23000  ordthmeolem  23168  ptcmplem2  23420  tuslem  23634  tuslemOLD  23635  dvnff  25303  bdayval  27012  noextend  27030  bdayfo  27041  vtxdgf  28461  fdifsuppconst  31650  ressupprn  31651  ofcfval3  32758  braew  32898  omsval  32950  sibfof  32997  sitmcl  33008  cndprobval  33090  hashfundm  33763  hashf1dmrn  33764  tailf  34893  tailfb  34895  ismgmOLD  36355  dfcnvrefrels2  37036  dfcnvrefrels3  37037  rclexi  41975  rtrclexlem  41976  cnvrcl0  41985  dfrtrcl5  41989  relexpmulg  42070  relexp01min  42073  relexpxpmin  42077  unidmex  43346  caragenval  44820  caragenunidm  44835  itcoval0  46834  itcoval1  46835
  Copyright terms: Public domain W3C validator