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

Theorem dmexg 5070
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  |-  ( A  e.  V  ->  dom  A  e.  _V )

Proof of Theorem dmexg
StepHypRef Expression
1 uniexg 4646 . 2  |-  ( A  e.  V  ->  U. A  e.  _V )
2 uniexg 4646 . 2  |-  ( U. A  e.  _V  ->  U.
U. A  e.  _V )
3 ssun1 3453 . . . 4  |-  dom  A  C_  ( dom  A  u.  ran  A )
4 dmrnssfld 5069 . . . 4  |-  ( dom 
A  u.  ran  A
)  C_  U. U. A
53, 4sstri 3300 . . 3  |-  dom  A  C_ 
U. U. A
6 ssexg 4290 . . 3  |-  ( ( dom  A  C_  U. U. A  /\  U. U. A  e.  _V )  ->  dom  A  e.  _V )
75, 6mpan 652 . 2  |-  ( U. U. A  e.  _V  ->  dom 
A  e.  _V )
81, 2, 73syl 19 1  |-  ( A  e.  V  ->  dom  A  e.  _V )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1717   _Vcvv 2899    u. cun 3261    C_ wss 3263   U.cuni 3957   dom cdm 4818   ran crn 4819
This theorem is referenced by:  dmex  5072  iprc  5074  exse2  5178  xpexr2  5248  soex  5259  cnvexg  5345  coexg  5352  dmfex  5566  cofunexg  5898  offval3  6257  tposexg  6429  tfrlem12  6586  tfrlem13  6587  erexb  6866  oion  7438  unxpwdom2  7489  wemapwe  7587  imadomg  8345  fpwwe2lem3  8441  fpwwe2lem12  8449  fpwwe2lem13  8450  hashfn  11576  o1of2  12333  prdsplusg  13608  prdsmulr  13609  prdsvsca  13610  prdshom  13616  ssclem  13946  ssc2  13949  ssctr  13952  subsubc  13977  resf1st  14018  resf2nd  14019  funcres  14020  spwex  14588  efgrcl  15274  dprdgrp  15490  dprdf  15491  dprdcntz  15493  dprddisj  15494  dprdw  15495  dprdssv  15501  dprdfid  15502  dprdfinv  15504  dprdfadd  15505  dprdfsub  15506  dprdfeq0  15507  dprdf11  15508  dprdlub  15511  dprdres  15513  dprdss  15514  dprdf1o  15517  subgdmdprd  15519  dmdprdsplitlem  15522  dprddisj2  15524  dprd2da  15527  dmdprdsplit2  15531  dpjfval  15540  dpjidcl  15543  ordtbaslem  17174  ordtuni  17176  ordtbas2  17177  ordtbas  17178  ordttopon  17179  ordtopn1  17180  ordtopn2  17181  ordtrest2lem  17189  ordtrest2  17190  txindislem  17586  ordthmeolem  17754  ptcmplem2  18005  tuslem  18218  mbfmulc2re  19407  mbfneg  19409  dvnff  19676  dchrptlem3  20917  fiusgraedgfi  21287  sizeusglecusg  21361  wlks  21390  wlkres  21393  trls  21400  crcts  21457  cycls  21458  vdusgraval  21526  vdgrnn0pnf  21528  hashnbgravdg  21530  usgravd0nedg  21531  iseupa  21535  ismgm  21756  ofcfval3  24281  braew  24387  cndprobval  24470  bdayval  25326  bdayfo  25353  tailf  26095  tailfb  26097  f1lindf  26961  xpexcnv  27327  vdgn0frgrav2  27778  vdgn1frgrav2  27780  vdgfrgragt2  27781
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-13 1719  ax-14 1721  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2368  ax-sep 4271  ax-nul 4279  ax-pr 4344  ax-un 4641
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2242  df-mo 2243  df-clab 2374  df-cleq 2380  df-clel 2383  df-nfc 2512  df-ne 2552  df-rex 2655  df-rab 2658  df-v 2901  df-dif 3266  df-un 3268  df-in 3270  df-ss 3277  df-nul 3572  df-if 3683  df-sn 3763  df-pr 3764  df-op 3766  df-uni 3958  df-br 4154  df-opab 4208  df-cnv 4826  df-dm 4828  df-rn 4829
  Copyright terms: Public domain W3C validator