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

Theorem rnexg 7603
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 7456 . 2 (𝐴𝑉 𝐴 ∈ V)
2 uniexg 7456 . 2 ( 𝐴 ∈ V → 𝐴 ∈ V)
3 ssun2 4146 . . . 4 ran 𝐴 ⊆ (dom 𝐴 ∪ ran 𝐴)
4 dmrnssfld 5834 . . . 4 (dom 𝐴 ∪ ran 𝐴) ⊆ 𝐴
53, 4sstri 3973 . . 3 ran 𝐴 𝐴
6 ssexg 5218 . . 3 ((ran 𝐴 𝐴 𝐴 ∈ V) → ran 𝐴 ∈ V)
75, 6mpan 686 . 2 ( 𝐴 ∈ V → ran 𝐴 ∈ V)
81, 2, 73syl 18 1 (𝐴𝑉 → ran 𝐴 ∈ V)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2105  Vcvv 3492  cun 3931  wss 3933   cuni 4830  dom cdm 5548  ran crn 5549
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-sep 5194  ax-nul 5201  ax-pr 5320  ax-un 7450
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2615  df-eu 2647  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-rex 3141  df-rab 3144  df-v 3494  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-nul 4289  df-if 4464  df-sn 4558  df-pr 4560  df-op 4564  df-uni 4831  df-br 5058  df-opab 5120  df-cnv 5556  df-dm 5558  df-rn 5559
This theorem is referenced by:  rnex  7606  imaexg  7609  xpexr  7612  xpexr2  7613  soex  7615  cnvexg  7618  coexg  7623  cofunexg  7639  funrnex  7644  abrexexg  7651  tposexg  7895  iunon  7965  onoviun  7969  tz7.44lem1  8030  tz7.44-3  8033  fopwdom  8613  disjen  8662  domss2  8664  domssex  8666  hartogslem2  8995  djuexb  9326  dfac12lem2  9558  unirnfdomd  9977  focdmex  13699  hashimarn  13789  trclexlem  14342  relexp0g  14369  relexpsucnnr  14372  restval  16688  prdsbas  16718  prdsplusg  16719  prdsmulr  16720  prdsvsca  16721  prdshom  16728  sscpwex  17073  sylow1lem4  18655  sylow3lem2  18682  sylow3lem3  18683  lsmvalx  18693  txindislem  22169  xkoptsub  22190  fmfnfmlem3  22492  fmfnfmlem4  22493  ustuqtoplem  22775  ustuqtop0  22776  utopsnneiplem  22783  efabl  25061  efsubm  25062  perpln1  26423  perpln2  26424  isperp  26425  lmif  26498  islmib  26500  isgrpo  28201  grpoinvfval  28226  grpodivfval  28238  isvcOLD  28283  isnv  28316  abrexexd  30196  acunirnmpt  30332  acunirnmpt2  30333  acunirnmpt2f  30334  fnpreimac  30344  locfinreflem  31003  esumrnmpt2  31226  sxsigon  31350  omssubadd  31457  carsgclctunlem2  31476  pmeasadd  31482  sitgclg  31499  bnj1366  32000  ptrest  34772  elghomlem1OLD  35044  elghomlem2OLD  35045  isrngod  35057  iscringd  35157  imaexALTV  35468  xrnresex  35534  dfcnvrefrels2  35646  dfcnvrefrels3  35647  lmhmlnmsplit  39565  rclexi  39853  rtrclexlem  39854  trclubgNEW  39856  cnvrcl0  39863  dfrtrcl5  39867  relexpmulg  39933  relexp01min  39936  relexpxpmin  39940  unirnmap  41347  unirnmapsn  41353  ssmapsn  41355  fourierdlem70  42338  fourierdlem71  42339  fourierdlem80  42348  meadjiunlem  42624  omeiunle  42676  fexafv2ex  43296
  Copyright terms: Public domain W3C validator