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

Theorem dmexg 7602
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 7456 . 2 (𝐴𝑉 𝐴 ∈ V)
2 uniexg 7456 . 2 ( 𝐴 ∈ V → 𝐴 ∈ V)
3 ssun1 4145 . . . 4 dom 𝐴 ⊆ (dom 𝐴 ∪ ran 𝐴)
4 dmrnssfld 5834 . . . 4 (dom 𝐴 ∪ ran 𝐴) ⊆ 𝐴
53, 4sstri 3973 . . 3 dom 𝐴 𝐴
6 ssexg 5218 . . 3 ((dom 𝐴 𝐴 𝐴 ∈ V) → dom 𝐴 ∈ V)
75, 6mpan 686 . 2 ( 𝐴 ∈ V → dom 𝐴 ∈ V)
81, 2, 73syl 18 1 (𝐴𝑉 → dom 𝐴 ∈ V)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2105  Vcvv 3492  cun 3931  wss 3933   cuni 4830  dom cdm 5548  ran crn 5549
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-sep 5194  ax-nul 5201  ax-pr 5320  ax-un 7450
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2615  df-eu 2647  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-rex 3141  df-rab 3144  df-v 3494  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-nul 4289  df-if 4464  df-sn 4558  df-pr 4560  df-op 4564  df-uni 4831  df-br 5058  df-opab 5120  df-cnv 5556  df-dm 5558  df-rn 5559
This theorem is referenced by:  dmexd  7604  dmex  7605  iprc  7607  exse2  7611  xpexr2  7613  xpexcnv  7614  soex  7615  cnvexg  7618  coexg  7623  dmfex  7630  cofunexg  7639  offval3  7672  opabn1stprc  7745  suppval  7821  funsssuppss  7845  suppss  7849  suppssov1  7851  suppssfv  7855  tposexg  7895  tfrlem12  8014  tfrlem13  8015  erexb  8303  f1vrnfibi  8797  oion  8988  fpwwe2lem3  10043  hashfn  13724  fundmge2nop0  13838  fun2dmnop0  13840  trclexlem  14342  relexp0g  14369  relexpsucnnr  14372  o1of2  14957  isofn  17033  ssclem  17077  ssc2  17080  ssctr  17083  subsubc  17111  resf1st  17152  resf2nd  17153  funcres  17154  dprddomprc  19051  dprdval0prc  19053  subgdmdprd  19085  dprd2da  19093  decpmatval0  21300  pmatcollpw3lem  21319  ordtbaslem  21724  ordtuni  21726  ordtbas2  21727  ordtbas  21728  ordttopon  21729  ordtopn1  21730  ordtopn2  21731  txindislem  22169  ordthmeolem  22337  ptcmplem2  22589  tuslem  22803  dvnff  24447  vtxdgf  27180  ofcfval3  31260  braew  31400  omsval  31450  sibfof  31497  sitmcl  31508  cndprobval  31590  hashfundm  32251  hashf1dmrn  32252  bdayval  33052  noextend  33070  bdayfo  33079  tailf  33620  tailfb  33622  ismgmOLD  35009  dfcnvrefrels2  35646  dfcnvrefrels3  35647  rclexi  39853  rtrclexlem  39854  cnvrcl0  39863  dfrtrcl5  39867  relexpmulg  39933  relexp01min  39936  relexpxpmin  39940  unidmex  41189  caragenval  42652  caragenunidm  42667
  Copyright terms: Public domain W3C validator