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

Theorem dmexg 6731
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

Proof of Theorem dmexg
StepHypRef Expression
1 uniexg 6597 . 2
2 uniexg 6597 . 2
3 ssun1 3666 . . . 4
4 dmrnssfld 5266 . . . 4
53, 4sstri 3512 . . 3
6 ssexg 4598 . . 3
75, 6mpan 670 . 2
81, 2, 73syl 20 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  e.wcel 1818   cvv 3109  u.cun 3473  C_wss 3475  U.cuni 4249  domcdm 5004  rancrn 5005
This theorem is referenced by:  dmex  6733  iprc  6735  exse2  6739  xpexr2  6741  xpexcnv  6742  soex  6743  cnvexg  6746  coexg  6751  dmfex  6758  cofunexg  6764  offval3  6794  suppval  6920  funsssuppss  6945  suppss  6949  suppssov1  6951  suppssfv  6955  tposexg  6988  tfrlem12  7077  tfrlem13  7078  erexb  7355  oion  7982  unxpwdom2  8035  wemapwe  8160  wemapweOLD  8161  imadomg  8933  fpwwe2lem3  9032  fpwwe2lem12  9040  fpwwe2lem13  9041  hashfn  12443  hashimarn  12496  o1of2  13435  prdsplusg  14855  prdsmulr  14856  prdsvsca  14857  prdshom  14864  ssclem  15188  ssc2  15191  ssctr  15194  subsubc  15222  resf1st  15263  resf2nd  15264  funcres  15265  efgrcl  16733  dprddomprc  17031  dprdval0prc  17033  dprdgrp  17038  dprdf  17039  dprdwOLD  17050  dprdssv  17056  dprdfidOLD  17064  dprdfinvOLD  17066  dprdfaddOLD  17067  dprdfsubOLD  17068  dprdfeq0OLD  17069  dprdf11OLD  17070  subgdmdprd  17081  dmdprdsplitlemOLD  17085  dprddisj2OLD  17088  dprd2da  17091  dpjidclOLD  17114  f1lindf  18857  decpmatval0  19265  pmatcollpw3lem  19284  ordtbaslem  19689  ordtuni  19691  ordtbas2  19692  ordtbas  19693  ordttopon  19694  ordtopn1  19695  ordtopn2  19696  ordtrest2lem  19704  ordtrest2  19705  txindislem  20134  ordthmeolem  20302  ptcmplem2  20553  tuslem  20770  mbfmulc2re  22055  mbfneg  22057  dvnff  22326  dchrptlem3  23541  fiusgraedgfi  24407  sizeusglecusg  24486  wlks  24519  wlkres  24522  trls  24538  crcts  24622  cycls  24623  vdusgraval  24907  vdgrnn0pnf  24909  hashnbgravdg  24913  usgravd0nedg  24918  iseupa  24965  vdgn0frgrav2  25024  vdgn1frgrav2  25026  vdgfrgragt2  25027  ismgmOLD  25322  ofcfval3  28101  braew  28214  omsval  28264  sibfof  28282  cndprobval  28372  bdayval  29408  bdayfo  29435  tailf  30193  tailfb  30195  f1vrnfibi  32313  isofn  32567
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-8 1820  ax-9 1822  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-sep 4573  ax-nul 4581  ax-pr 4691  ax-un 6592
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-eu 2286  df-mo 2287  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-rex 2813  df-rab 2816  df-v 3111  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-sn 4030  df-pr 4032  df-op 4036  df-uni 4250  df-br 4453  df-opab 4511  df-cnv 5012  df-dm 5014  df-rn 5015
  Copyright terms: Public domain W3C validator