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

Theorem dmexg 7094
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 6952 . 2 (𝐴𝑉 𝐴 ∈ V)
2 uniexg 6952 . 2 ( 𝐴 ∈ V → 𝐴 ∈ V)
3 ssun1 3774 . . . 4 dom 𝐴 ⊆ (dom 𝐴 ∪ ran 𝐴)
4 dmrnssfld 5382 . . . 4 (dom 𝐴 ∪ ran 𝐴) ⊆ 𝐴
53, 4sstri 3610 . . 3 dom 𝐴 𝐴
6 ssexg 4802 . . 3 ((dom 𝐴 𝐴 𝐴 ∈ V) → dom 𝐴 ∈ V)
75, 6mpan 706 . 2 ( 𝐴 ∈ V → dom 𝐴 ∈ V)
81, 2, 73syl 18 1 (𝐴𝑉 → dom 𝐴 ∈ V)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1989  Vcvv 3198  cun 3570  wss 3572   cuni 4434  dom cdm 5112  ran crn 5113
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1721  ax-4 1736  ax-5 1838  ax-6 1887  ax-7 1934  ax-8 1991  ax-9 1998  ax-10 2018  ax-11 2033  ax-12 2046  ax-13 2245  ax-ext 2601  ax-sep 4779  ax-nul 4787  ax-pr 4904  ax-un 6946
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1485  df-ex 1704  df-nf 1709  df-sb 1880  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2752  df-rex 2917  df-rab 2920  df-v 3200  df-dif 3575  df-un 3577  df-in 3579  df-ss 3586  df-nul 3914  df-if 4085  df-sn 4176  df-pr 4178  df-op 4182  df-uni 4435  df-br 4652  df-opab 4711  df-cnv 5120  df-dm 5122  df-rn 5123
This theorem is referenced by:  dmex  7096  iprc  7098  exse2  7102  xpexr2  7104  xpexcnv  7105  soex  7106  cnvexg  7109  coexg  7114  dmfex  7121  cofunexg  7127  offval3  7159  opabn1stprc  7225  suppval  7294  funsssuppss  7318  suppss  7322  suppssov1  7324  suppssfv  7328  tposexg  7363  tfrlem12  7482  tfrlem13  7483  erexb  7764  f1vrnfibi  8248  oion  8438  unxpwdom2  8490  wemapwe  8591  imadomg  9353  fpwwe2lem3  9452  fpwwe2lem12  9460  fpwwe2lem13  9461  hashfn  13159  hashdmpropge2  13260  fundmge2nop0  13269  fun2dmnop0  13271  trclexlem  13727  relexp0g  13756  relexpsucnnr  13759  o1of2  14337  prdsplusg  16112  prdsmulr  16113  prdsvsca  16114  prdshom  16121  isofn  16429  ssclem  16473  ssc2  16476  ssctr  16479  subsubc  16507  resf1st  16548  resf2nd  16549  funcres  16550  efgrcl  18122  dprddomprc  18393  dprdval0prc  18395  dprdgrp  18398  dprdf  18399  dprdssv  18409  subgdmdprd  18427  dprd2da  18435  f1lindf  20155  decpmatval0  20563  pmatcollpw3lem  20582  ordtbaslem  20986  ordtuni  20988  ordtbas2  20989  ordtbas  20990  ordttopon  20991  ordtopn1  20992  ordtopn2  20993  ordtrest2lem  21001  ordtrest2  21002  txindislem  21430  ordthmeolem  21598  ptcmplem2  21851  tuslem  22065  mbfmulc2re  23409  mbfneg  23411  dvnff  23680  dchrptlem3  24985  structgrssvtxlemOLD  25909  vtxdgf  26361  gsummpt2d  29766  ofcfval3  30149  braew  30290  omsval  30340  sibfof  30387  sitmcl  30398  cndprobval  30480  bdayval  31785  noextend  31803  bdayfo  31812  tailf  32354  tailfb  32356  ismgmOLD  33629  rclexi  37748  rtrclexlem  37749  trclubgNEW  37751  cnvrcl0  37758  dfrtrcl5  37762  relexpmulg  37828  relexp01min  37831  relexpxpmin  37835  unidmex  39043  dmexd  39244  caragenval  40476  omecl  40486  caragenunidm  40491  offval0  42070
  Copyright terms: Public domain W3C validator