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

Theorem dmexg 6963
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 6827 . 2 (𝐴𝑉 𝐴 ∈ V)
2 uniexg 6827 . 2 ( 𝐴 ∈ V → 𝐴 ∈ V)
3 ssun1 3734 . . . 4 dom 𝐴 ⊆ (dom 𝐴 ∪ ran 𝐴)
4 dmrnssfld 5289 . . . 4 (dom 𝐴 ∪ ran 𝐴) ⊆ 𝐴
53, 4sstri 3573 . . 3 dom 𝐴 𝐴
6 ssexg 4724 . . 3 ((dom 𝐴 𝐴 𝐴 ∈ V) → dom 𝐴 ∈ V)
75, 6mpan 701 . 2 ( 𝐴 ∈ V → dom 𝐴 ∈ V)
81, 2, 73syl 18 1 (𝐴𝑉 → dom 𝐴 ∈ V)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1976  Vcvv 3169  cun 3534  wss 3536   cuni 4363  dom cdm 5025  ran crn 5026
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2229  ax-ext 2586  ax-sep 4700  ax-nul 4709  ax-pr 4825  ax-un 6821
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2458  df-mo 2459  df-clab 2593  df-cleq 2599  df-clel 2602  df-nfc 2736  df-rex 2898  df-rab 2901  df-v 3171  df-dif 3539  df-un 3541  df-in 3543  df-ss 3550  df-nul 3871  df-if 4033  df-sn 4122  df-pr 4124  df-op 4128  df-uni 4364  df-br 4575  df-opab 4635  df-cnv 5033  df-dm 5035  df-rn 5036
This theorem is referenced by:  dmex  6965  iprc  6967  exse2  6972  xpexr2  6974  xpexcnv  6975  soex  6976  cnvexg  6979  coexg  6984  dmfex  6991  cofunexg  6997  offval3  7027  suppval  7158  funsssuppss  7182  suppss  7186  suppssov1  7188  suppssfv  7192  tposexg  7227  tfrlem12  7346  tfrlem13  7347  erexb  7628  f1vrnfibi  8108  oion  8298  unxpwdom2  8350  wemapwe  8451  imadomg  9211  fpwwe2lem3  9308  fpwwe2lem12  9316  fpwwe2lem13  9317  hashfn  12974  trclexlem  13524  relexp0g  13553  relexpsucnnr  13556  o1of2  14134  prdsplusg  15884  prdsmulr  15885  prdsvsca  15886  prdshom  15893  isofn  16201  ssclem  16245  ssc2  16248  ssctr  16251  subsubc  16279  resf1st  16320  resf2nd  16321  funcres  16322  efgrcl  17894  dprddomprc  18165  dprdval0prc  18167  dprdgrp  18170  dprdf  18171  dprdssv  18181  subgdmdprd  18199  dprd2da  18207  f1lindf  19919  decpmatval0  20327  pmatcollpw3lem  20346  ordtbaslem  20741  ordtuni  20743  ordtbas2  20744  ordtbas  20745  ordttopon  20746  ordtopn1  20747  ordtopn2  20748  ordtrest2lem  20756  ordtrest2  20757  txindislem  21185  ordthmeolem  21353  ptcmplem2  21606  tuslem  21820  mbfmulc2re  23135  mbfneg  23137  dvnff  23406  dchrptlem3  24705  fiusgraedgfi  25699  sizeusglecusg  25777  wlks  25810  wlkres  25813  trls  25829  crcts  25913  cycls  25914  vdusgraval  26197  vdgrnn0pnf  26199  hashnbgravdg  26203  usgravd0nedg  26208  iseupa  26255  vdgn0frgrav2  26314  vdgn1frgrav2  26316  vdgfrgragt2  26317  gsummpt2d  28915  ofcfval3  29294  braew  29435  omsval  29485  sibfof  29532  sitmcl  29543  cndprobval  29625  bdayval  30848  bdayfo  30877  tailf  31343  tailfb  31345  ismgmOLD  32619  rclexi  36741  rtrclexlem  36742  trclubgNEW  36744  cnvrcl0  36751  dfrtrcl5  36755  relexpmulg  36821  relexp01min  36824  relexpxpmin  36828  unidmex  38042  dmexd  38217  caragenval  39184  omecl  39194  caragenunidm  39199  opabn1stprc  40130  fundmge2nop0  40149  fun2dmnop0  40151  structgrssvtxlem  40255  vtxdgf  40685  offval0  42092
  Copyright terms: Public domain W3C validator