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

Theorem rnexg 7600
 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 7451 . 2 (𝐴𝑉 𝐴 ∈ V)
2 uniexg 7451 . 2 ( 𝐴 ∈ V → 𝐴 ∈ V)
3 ssun2 4124 . . . 4 ran 𝐴 ⊆ (dom 𝐴 ∪ ran 𝐴)
4 dmrnssfld 5819 . . . 4 (dom 𝐴 ∪ ran 𝐴) ⊆ 𝐴
53, 4sstri 3951 . . 3 ran 𝐴 𝐴
6 ssexg 5203 . . 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 2114  Vcvv 3469   ∪ cun 3906   ⊆ wss 3908  ∪ cuni 4813  dom cdm 5532  ran crn 5533 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2178  ax-ext 2794  ax-sep 5179  ax-nul 5186  ax-pr 5307  ax-un 7446 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2622  df-eu 2653  df-clab 2801  df-cleq 2815  df-clel 2894  df-nfc 2962  df-rab 3139  df-v 3471  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4266  df-if 4440  df-sn 4540  df-pr 4542  df-op 4546  df-uni 4814  df-br 5043  df-opab 5105  df-cnv 5540  df-dm 5542  df-rn 5543 This theorem is referenced by:  rnex  7603  imaexg  7606  xpexr  7609  xpexr2  7610  soex  7612  cnvexg  7615  coexg  7620  cofunexg  7636  funrnex  7641  abrexexg  7648  tposexg  7893  iunon  7963  onoviun  7967  tz7.44lem1  8028  tz7.44-3  8031  fopwdom  8612  disjen  8662  domss2  8664  domssex  8666  hartogslem2  8995  djuexb  9326  dfac12lem2  9559  unirnfdomd  9978  focdmex  13707  hashimarn  13797  trclexlem  14345  relexp0g  14372  relexpsucnnr  14375  restval  16691  prdsbas  16721  prdsplusg  16722  prdsmulr  16723  prdsvsca  16724  prdshom  16731  sscpwex  17076  sylow1lem4  18717  sylow3lem2  18744  sylow3lem3  18745  lsmvalx  18755  txindislem  22236  xkoptsub  22257  fmfnfmlem3  22559  fmfnfmlem4  22560  ustuqtoplem  22843  ustuqtop0  22844  utopsnneiplem  22851  efabl  25140  efsubm  25141  perpln1  26502  perpln2  26503  isperp  26504  lmif  26577  islmib  26579  isgrpo  28278  grpoinvfval  28303  grpodivfval  28315  isvcOLD  28360  isnv  28393  abrexexd  30275  acunirnmpt  30412  acunirnmpt2  30413  acunirnmpt2f  30414  fnpreimac  30424  locfinreflem  31162  esumrnmpt2  31401  sxsigon  31525  omssubadd  31632  carsgclctunlem2  31651  pmeasadd  31657  sitgclg  31674  bnj1366  32175  ptrest  35014  elghomlem1OLD  35281  elghomlem2OLD  35282  isrngod  35294  iscringd  35394  imaexALTV  35705  xrnresex  35772  dfcnvrefrels2  35884  dfcnvrefrels3  35885  lmhmlnmsplit  39961  rclexi  40245  rtrclexlem  40246  trclubgNEW  40248  cnvrcl0  40255  dfrtrcl5  40259  relexpmulg  40341  relexp01min  40344  relexpxpmin  40348  unirnmap  41775  unirnmapsn  41781  ssmapsn  41783  fourierdlem70  42757  fourierdlem71  42758  fourierdlem80  42767  meadjiunlem  43043  omeiunle  43095  fexafv2ex  43715
 Copyright terms: Public domain W3C validator