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

Theorem rnexg 7842
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 (𝐴𝑉 → ran 𝐴 ∈ V)

Proof of Theorem rnexg
StepHypRef Expression
1 uniexg 7678 . 2 (𝐴𝑉 𝐴 ∈ V)
2 uniexg 7678 . 2 ( 𝐴 ∈ V → 𝐴 ∈ V)
3 ssun2 4134 . . . 4 ran 𝐴 ⊆ (dom 𝐴 ∪ ran 𝐴)
4 dmrnssfld 5926 . . . 4 (dom 𝐴 ∪ ran 𝐴) ⊆ 𝐴
53, 4sstri 3954 . . 3 ran 𝐴 𝐴
6 ssexg 5281 . . 3 ((ran 𝐴 𝐴 𝐴 ∈ V) → ran 𝐴 ∈ V)
75, 6mpan 689 . 2 ( 𝐴 ∈ V → ran 𝐴 ∈ V)
81, 2, 73syl 18 1 (𝐴𝑉 → ran 𝐴 ∈ V)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2107  Vcvv 3444  cun 3909  wss 3911   cuni 4866  dom cdm 5634  ran crn 5635
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-sep 5257  ax-nul 5264  ax-pr 5385  ax-un 7673
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3407  df-v 3446  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4284  df-if 4488  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4867  df-br 5107  df-opab 5169  df-cnv 5642  df-dm 5644  df-rn 5645
This theorem is referenced by:  rnex  7850  imaexg  7853  xpexr  7856  xpexr2  7857  soex  7859  cnvexg  7862  coexg  7867  cofunexg  7882  funrnex  7887  abrexexgOLD  7895  tposexg  8172  iunon  8286  onoviun  8290  tz7.44lem1  8352  tz7.44-3  8355  fopwdom  9027  disjen  9081  domss2  9083  domssex  9085  hartogslem2  9484  ttrclexg  9664  djuexb  9850  dfac12lem2  10085  unirnfdomd  10508  hashimarn  14346  trclexlem  14885  relexp0g  14913  relexpsucnnr  14916  restval  17313  prdsbas  17344  prdsplusg  17345  prdsmulr  17346  prdsvsca  17347  prdshom  17354  sscpwex  17703  sylow1lem4  19388  sylow3lem2  19415  sylow3lem3  19416  lsmvalx  19426  txindislem  23000  xkoptsub  23021  fmfnfmlem3  23323  fmfnfmlem4  23324  ustuqtoplem  23607  ustuqtop0  23608  utopsnneiplem  23615  efabl  25922  efsubm  25923  addsunif  27332  perpln1  27694  perpln2  27695  isperp  27696  lmif  27769  islmib  27771  isgrpo  29481  grpoinvfval  29506  grpodivfval  29518  isvcOLD  29563  isnv  29596  abrexexd  31478  acunirnmpt  31621  acunirnmpt2  31622  acunirnmpt2f  31623  fnpreimac  31633  rnexd  31641  locfinreflem  32478  esumrnmpt2  32724  sxsigon  32848  omssubadd  32957  carsgclctunlem2  32976  pmeasadd  32982  sitgclg  32999  bnj1366  33498  ptrest  36123  elghomlem1OLD  36390  elghomlem2OLD  36391  isrngod  36403  iscringd  36503  imaexALTV  36837  xrnresex  36914  dfcnvrefrels2  37036  dfcnvrefrels3  37037  sticksstones3  40602  lmhmlnmsplit  41457  rclexi  41975  rtrclexlem  41976  trclubgNEW  41978  cnvrcl0  41985  dfrtrcl5  41989  relexpmulg  42070  relexp01min  42073  relexpxpmin  42077  unirnmap  43516  unirnmapsn  43522  ssmapsn  43524  fourierdlem70  44503  fourierdlem71  44504  fourierdlem80  44513  meadjiunlem  44792  omeiunle  44844  fexafv2ex  45538
  Copyright terms: Public domain W3C validator