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

Theorem rnexg 6732
Description: The range of a set is a set. Corollary 6.8(3) of [TakeutiZaring] p. 26. Similar to Lemma 3D of [Enderton] p. 41. (Contributed by NM, 31-Mar-1995.)
Assertion
Ref Expression
rnexg

Proof of Theorem rnexg
StepHypRef Expression
1 uniexg 6597 . 2
2 uniexg 6597 . 2
3 ssun2 3667 . . . 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:  rnex  6734  imaexg  6737  xpexr  6740  xpexr2  6741  soex  6743  cnvexg  6746  coexg  6751  cofunexg  6764  funrnex  6767  abrexexg  6775  tposexg  6988  iunon  7028  onoviun  7033  tz7.44lem1  7090  tz7.44-3  7093  fopwdom  7645  disjen  7694  domss2  7696  domssex  7698  hartogslem2  7989  dfac12lem2  8545  unirnfdomd  8963  hashf1rn  12425  hashimarn  12496  restval  14824  prdsbas  14854  prdsplusg  14855  prdsmulr  14856  prdsvsca  14857  prdshom  14864  sscpwex  15184  sylow1lem4  16621  sylow3lem2  16648  sylow3lem3  16649  lsmvalx  16659  txindislem  20134  xkoptsub  20155  fmfnfmlem3  20457  fmfnfmlem4  20458  ustuqtoplem  20742  ustuqtop0  20743  utopsnneiplem  20750  efabl  22937  efsubm  22938  perpln1  24087  perpln2  24088  isperp  24089  lmif  24151  islmib  24153  sizeusglecusg  24486  isgrpo  25198  grpoinvfval  25226  grpodivfval  25244  gxfval  25259  issubgoi  25312  elghomlem1OLD  25363  elghomlem2OLD  25364  ghgrpOLD  25370  isrngod  25381  isvc  25474  isnv  25505  abrexexd  27407  locfinreflem  27843  sxsigon  28163  sitgclg  28284  ptrest  30048  iscringd  30396  lmhmlnmsplit  31033  fourierdlem70  31959  fourierdlem71  31960  fourierdlem80  31969  bnj1366  33888
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