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

Theorem dmexg 6500
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 6368 . 2  |-  ( A  e.  V  ->  U. A  e.  _V )
2 uniexg 6368 . 2  |-  ( U. A  e.  _V  ->  U.
U. A  e.  _V )
3 ssun1 3509 . . . 4  |-  dom  A  C_  ( dom  A  u.  ran  A )
4 dmrnssfld 5087 . . . 4  |-  ( dom 
A  u.  ran  A
)  C_  U. U. A
53, 4sstri 3355 . . 3  |-  dom  A  C_ 
U. U. A
6 ssexg 4428 . . 3  |-  ( ( dom  A  C_  U. U. A  /\  U. U. A  e.  _V )  ->  dom  A  e.  _V )
75, 6mpan 665 . 2  |-  ( U. U. A  e.  _V  ->  dom 
A  e.  _V )
81, 2, 73syl 20 1  |-  ( A  e.  V  ->  dom  A  e.  _V )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1757   _Vcvv 2964    u. cun 3316    C_ wss 3318   U.cuni 4081   dom cdm 4829   ran crn 4830
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1671  ax-6 1709  ax-7 1729  ax-8 1759  ax-9 1761  ax-10 1776  ax-11 1781  ax-12 1793  ax-13 1944  ax-ext 2416  ax-sep 4403  ax-nul 4411  ax-pr 4521  ax-un 6363
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 962  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1702  df-eu 2260  df-mo 2261  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ne 2600  df-rex 2713  df-rab 2716  df-v 2966  df-dif 3321  df-un 3323  df-in 3325  df-ss 3332  df-nul 3628  df-if 3782  df-sn 3868  df-pr 3870  df-op 3874  df-uni 4082  df-br 4283  df-opab 4341  df-cnv 4837  df-dm 4839  df-rn 4840
This theorem is referenced by:  dmex  6502  iprc  6504  exse2  6508  xpexr2  6510  xpexcnv  6511  soex  6512  cnvexg  6515  coexg  6519  dmfex  6526  cofunexg  6532  offval3  6562  suppval  6683  funsssuppss  6706  suppss  6710  suppssov1  6712  suppssfv  6716  tposexg  6750  tfrlem12  6836  tfrlem13  6837  erexb  7116  oion  7740  unxpwdom2  7793  wemapwe  7918  wemapweOLD  7919  imadomg  8691  fpwwe2lem3  8790  fpwwe2lem12  8798  fpwwe2lem13  8799  hashfn  12124  hashimarn  12186  o1of2  13076  prdsplusg  14381  prdsmulr  14382  prdsvsca  14383  prdshom  14390  ssclem  14717  ssc2  14720  ssctr  14723  subsubc  14748  resf1st  14789  resf2nd  14790  funcres  14791  efgrcl  16194  dprddomprc  16458  dprdval0prc  16460  dprdgrp  16465  dprdf  16466  dprdcntz  16468  dprddisj  16469  dprdw  16470  dprdwOLD  16476  dprdssv  16482  dprdfeq0  16488  dprdf11  16489  dprdfidOLD  16490  dprdfinvOLD  16492  dprdfaddOLD  16493  dprdfsubOLD  16494  dprdfeq0OLD  16495  dprdf11OLD  16496  dprdres  16501  dprdf1o  16505  subgdmdprd  16507  dmdprdsplitlemOLD  16511  dprddisj2OLD  16514  dprd2da  16517  dmdprdsplit2  16521  dpjfval  16530  dpjidclOLD  16540  f1lindf  18095  ordtbaslem  18636  ordtuni  18638  ordtbas2  18639  ordtbas  18640  ordttopon  18641  ordtopn1  18642  ordtopn2  18643  ordtrest2lem  18651  ordtrest2  18652  txindislem  19050  ordthmeolem  19218  ptcmplem2  19469  tuslem  19686  mbfmulc2re  20970  mbfneg  20972  dvnff  21241  dchrptlem3  22492  fiusgraedgfi  23145  sizeusglecusg  23219  wlks  23250  wlkres  23253  trls  23260  crcts  23333  cycls  23334  vdusgraval  23402  vdgrnn0pnf  23404  hashnbgravdg  23406  usgravd0nedg  23407  iseupa  23411  ismgm  23632  ofcfval3  26400  braew  26514  sibfof  26576  cndprobval  26666  bdayval  27638  bdayfo  27665  tailf  28442  tailfb  28444  vdgn0frgrav2  30465  vdgn1frgrav2  30467  vdgfrgragt2  30468
  Copyright terms: Public domain W3C validator